Definition df-rn 5322

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 27624). Contrast with domain (defined in df-dm 5321). For alternate definitions, see dfrn2 5512, dfrn3 5513, and dfrn4 5806. 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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	crn 5312	. 2 class ran 𝐴
3	1	ccnv 5310	. . 3 class ◡𝐴
4	3	cdm 5311	. 2 class dom ◡𝐴
5	2, 4	wceq 1637	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5512  dmcnvcnv  5549  rncnvcnv  5550  rneq  5552  rnss  5555  brelrng  5556  nfrn  5569  rncoss  5587  rncoeq  5590  cnvimarndm  5696  rnun  5752  rnin  5753  rnxp  5775  rnxpss  5777  imainrect  5786  rnsnopg  5826  cnvssrndm  5871  unidmrn  5879  dfdm2  5881  funcnvpr  6158  funcnvtp  6159  funcnvqp  6160  fncnv  6169  funcnvres  6174  funimacnv  6177  fimacnvdisj  6294  dff1o4  6357  foimacnv  6366  funcocnv2  6373  f1ompt  6599  nvof1o  6756  cnvexg  7338  tz7.48-3  7771  errn  7997  omxpenlem  8296  sbthlem5  8309  sbthlem8  8312  sbthlem9  8313  fodomr  8346  domss2  8354  rnfi  8484  zorn2lem4  9602  rnct  9628  fpwwe2lem13  9745  trclublem  13955  relexpcnv  13994  relexpnnrn  14004  invf  16628  cicsym  16664  cnvtsr  17423  znleval  20106  ordtbas2  21205  ordtcnv  21215  ordtrest2  21218  cnconn  21435  tgqtop  21725  adj1o  29077  fcoinver  29739  fresf1o  29756  fcnvgreu  29795  dfcnv2  29799  cnvordtrestixx  30280  xrge0iifhmeo  30303  mbfmcst  30642  0rrv  30834  elrn3  31969  dfrn6  34383  cnvresrn  34424  dmcoss2  34512  cnvrcl0  38426  conrel2d  38450  relexpaddss  38504  rntrclfvRP  38517  ntrneifv2  38872