Definition df-rn 5696

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30459). Contrast with domain (defined in df-dm 5695). For alternate definitions, see dfrn2 5899, dfrn3 5900, and dfrn4 6222. The notation "ran " is used by Enderton. The range of a function is often also called "the image of the function" (see definition in [Lang] p. ix), which can be justified by imadmrn 6088. Not to be confused with "codomain" (see df-f 6565), which may be a superset/superclass of the range (see frn 6743). (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 5686	. 2 class ran 𝐴
3	1	ccnv 5684	. . 3 class ◡𝐴
4	3	cdm 5685	. 2 class dom ◡𝐴
5	2, 4	wceq 1540	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5899  dmcnvcnv  5944  rncnvcnv  5945  rneq  5947  rnss  5950  brelrng  5952  nfrn  5963  rncoss  5986  rncoeq  5990  cnvimarndm  6101  rnun  6165  rnin  6166  rnxp  6190  rnxpss  6192  imainrect  6201  rnsnopg  6241  cnvssrndm  6291  unidmrn  6299  dfdm2  6301  funcnvpr  6628  funcnvtp  6629  funcnvqp  6630  fncnv  6639  funcnvres  6644  funimacnv  6647  fimacnvdisj  6786  dff1o4  6856  foimacnv  6865  funcocnv2  6873  f1ompt  7131  nvof1o  7300  cnvexg  7946  tz7.48-3  8484  errn  8767  omxpenlem  9113  sbthlem5  9127  sbthlem8  9130  sbthlem9  9131  fodomr  9168  domss2  9176  fodomfir  9368  rnfi  9380  zorn2lem4  10539  rnct  10565  fpwwe2lem12  10682  trclublem  15034  relexpcnv  15074  relexpnnrn  15084  invf  17812  cicsym  17848  cnvtsr  18633  znleval  21573  ordtbas2  23199  ordtcnv  23209  ordtrest2  23212  cnconn  23430  tgqtop  23720  adj1o  31913  fcoinver  32617  fresf1o  32641  fcnvgreu  32683  dfcnv2  32686  preiman0  32719  gsumhashmul  33064  cycpmfvlem  33132  cycpmfv1  33133  cycpmfv2  33134  cycpmfv3  33135  cycpmrn  33163  cnvordtrestixx  33912  xrge0iifhmeo  33935  mbfmcst  34261  0rrv  34453  elrn3  35762  dfrn6  38303  cnvresrn  38349  dmcoss2  38455  cnvrcl0  43638  conrel2d  43677  relexpaddss  43731  rntrclfvRP  43744  ntrneifv2  44093