Definition df-rn 5699

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30468). Contrast with domain (defined in df-dm 5698). For alternate definitions, see dfrn2 5901, dfrn3 5902, and dfrn4 6223. 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 6089. Not to be confused with "codomain" (see df-f 6566), 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 5689	. 2 class ran 𝐴
3	1	ccnv 5687	. . 3 class ◡𝐴
4	3	cdm 5688	. 2 class dom ◡𝐴
5	2, 4	wceq 1536	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5901  dmcnvcnv  5946  rncnvcnv  5947  rneq  5949  rnss  5952  brelrng  5954  nfrn  5965  rncoss  5988  rncoeq  5992  cnvimarndm  6102  rnun  6167  rnin  6168  rnxp  6191  rnxpss  6193  imainrect  6202  rnsnopg  6242  cnvssrndm  6292  unidmrn  6300  dfdm2  6302  funcnvpr  6629  funcnvtp  6630  funcnvqp  6631  fncnv  6640  funcnvres  6645  funimacnv  6648  fimacnvdisj  6786  dff1o4  6856  foimacnv  6865  funcocnv2  6873  f1ompt  7130  nvof1o  7299  cnvexg  7946  tz7.48-3  8482  errn  8765  omxpenlem  9111  sbthlem5  9125  sbthlem8  9128  sbthlem9  9129  fodomr  9166  domss2  9174  fodomfir  9365  rnfi  9377  zorn2lem4  10536  rnct  10562  fpwwe2lem12  10679  trclublem  15030  relexpcnv  15070  relexpnnrn  15080  invf  17815  cicsym  17851  cnvtsr  18645  znleval  21590  ordtbas2  23214  ordtcnv  23224  ordtrest2  23227  cnconn  23445  tgqtop  23735  adj1o  31922  fcoinver  32623  fresf1o  32647  fcnvgreu  32689  dfcnv2  32692  preiman0  32724  gsumhashmul  33046  cycpmfvlem  33114  cycpmfv1  33115  cycpmfv2  33116  cycpmfv3  33117  cycpmrn  33145  cnvordtrestixx  33873  xrge0iifhmeo  33896  mbfmcst  34240  0rrv  34432  elrn3  35741  dfrn6  38283  cnvresrn  38329  dmcoss2  38435  cnvrcl0  43614  conrel2d  43653  relexpaddss  43707  rntrclfvRP  43720  ntrneifv2  44069