MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rn Structured version   Visualization version   GIF version

Definition df-rn 5049
Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 26689). Contrast with domain (defined in df-dm 5048). For alternate definitions, see dfrn2 5233, dfrn3 5234, and dfrn4 5513. The notation "ran " is used by Enderton; other authors sometimes use script R or script W. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-rn ran 𝐴 = dom 𝐴

Detailed syntax breakdown of Definition df-rn
StepHypRef Expression
1 cA . . 3 class 𝐴
21crn 5039 . 2 class ran 𝐴
31ccnv 5037 . . 3 class 𝐴
43cdm 5038 . 2 class dom 𝐴
52, 4wceq 1475 1 wff ran 𝐴 = dom 𝐴
Colors of variables: wff setvar class
This definition is referenced by:  dfrn2  5233  dmcnvcnv  5269  rncnvcnv  5270  rneq  5272  rnss  5275  brelrng  5276  nfrn  5289  rncoss  5307  rncoeq  5310  cnvimarndm  5405  rnun  5460  rnin  5461  rnxp  5483  rnxpss  5485  imainrect  5494  rnsnopg  5532  cnvssrndm  5574  unidmrn  5582  dfdm2  5584  funcnvpr  5864  funcnvtp  5865  funcnvqp  5866  funcnvqpOLD  5867  fncnv  5876  funcnvres  5881  funimacnv  5884  fimacnvdisj  5996  dff1o4  6058  foimacnv  6067  funcocnv2  6074  f1ompt  6290  nvof1o  6436  cnvexg  7005  tz7.48-3  7426  errn  7651  omxpenlem  7946  sbthlem5  7959  sbthlem8  7962  sbthlem9  7963  fodomr  7996  domss2  8004  rnfi  8132  zorn2lem4  9204  fpwwe2lem13  9343  trclublem  13582  relexpcnv  13623  relexpnnrn  13633  invf  16251  cicsym  16287  cnvtsr  17045  znleval  19722  ordtbas2  20805  ordtcnv  20815  ordtrest2  20818  cnconn  21035  tgqtop  21325  adj1o  28137  fcoinver  28798  fresf1o  28815  fcnvgreu  28855  dfcnv2  28859  rnct  28879  cnvordtrestixx  29287  xrge0iifhmeo  29310  mbfmcst  29648  0rrv  29840  elrn3  30906  cnvrcl0  36951  conrel2d  36975  relexpaddss  37029  rntrclfvRP  37042  ntrneifv2  37398
  Copyright terms: Public domain W3C validator