Definition df-rn 5631

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30530). Contrast with domain (defined in df-dm 5630). For alternate definitions, see dfrn2 5836, dfrn3 5837, and dfrn4 6156. 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 6028. Not to be confused with "codomain" (see df-f 6492), which may be a superset/superclass of the range (see frn 6665). (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 5621	. 2 class ran 𝐴
3	1	ccnv 5619	. . 3 class ◡𝐴
4	3	cdm 5620	. 2 class dom ◡𝐴
5	2, 4	wceq 1548	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5836  dmcnvcnv  5881  rncnvcnv  5882  rneq  5884  rnss  5887  brelrng  5889  nfrn  5900  rncoss  5925  rncoeq  5930  cnvimarndm  6041  rnun  6098  rninOLD  6100  rnxp  6124  rnxpss  6126  imainrect  6135  rnsnopg  6175  cnvssrndm  6225  unidmrn  6233  dfdm2  6235  funcnvpr  6550  funcnvtp  6551  funcnvqp  6552  fncnv  6561  funcnvres  6566  funimacnv  6569  fimacnvdisj  6708  dff1o4  6778  foimacnv  6787  funcocnv2  6795  f1ompt  7055  nvof1o  7227  cnvexg  7868  tz7.48-3  8377  errn  8660  omxpenlem  9010  sbthlem5  9023  sbthlem8  9026  sbthlem9  9027  fodomr  9060  domss2  9068  fodomfir  9232  rnfi  9244  zorn2lem4  10417  rnct  10443  fpwwe2lem12  10561  trclublem  14952  relexpcnv  14992  relexpnnrn  15002  invf  17730  cicsym  17766  cnvtsr  18549  znleval  21532  ordtbas2  23177  ordtcnv  23187  ordtrest2  23190  cnconn  23408  tgqtop  23698  adj1o  31985  fcoinver  32695  fresf1o  32725  fcnvgreu  32766  dfcnv2  32769  preiman0  32804  gsumhashmul  33150  cycpmfvlem  33195  cycpmfv1  33196  cycpmfv2  33197  cycpmfv3  33198  cycpmrn  33226  cnvordtrestixx  34107  xrge0iifhmeo  34130  mbfmcst  34453  0rrv  34645  elrn3  36003  dfrn6  38688  cnvresrn  38728  dmxrn  38767  dmcoss2  38924  cnvrcl0  44082  conrel2d  44121  relexpaddss  44175  rntrclfvRP  44188  ntrneifv2  44537