Definition df-rn 5625

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30420). Contrast with domain (defined in df-dm 5624). For alternate definitions, see dfrn2 5827, dfrn3 5828, and dfrn4 6149. 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 6018. Not to be confused with "codomain" (see df-f 6485), which may be a superset/superclass of the range (see frn 6658). (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 5615	. 2 class ran 𝐴
3	1	ccnv 5613	. . 3 class ◡𝐴
4	3	cdm 5614	. 2 class dom ◡𝐴
5	2, 4	wceq 1541	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5827  dmcnvcnv  5872  rncnvcnv  5873  rneq  5875  rnss  5878  brelrng  5880  nfrn  5891  rncoss  5915  rncoeq  5920  cnvimarndm  6031  rnun  6092  rnin  6093  rnxp  6117  rnxpss  6119  imainrect  6128  rnsnopg  6168  cnvssrndm  6218  unidmrn  6226  dfdm2  6228  funcnvpr  6543  funcnvtp  6544  funcnvqp  6545  fncnv  6554  funcnvres  6559  funimacnv  6562  fimacnvdisj  6701  dff1o4  6771  foimacnv  6780  funcocnv2  6788  f1ompt  7044  nvof1o  7214  cnvexg  7854  tz7.48-3  8363  errn  8644  omxpenlem  8991  sbthlem5  9004  sbthlem8  9007  sbthlem9  9008  fodomr  9041  domss2  9049  fodomfir  9212  rnfi  9224  zorn2lem4  10390  rnct  10416  fpwwe2lem12  10533  trclublem  14902  relexpcnv  14942  relexpnnrn  14952  invf  17675  cicsym  17711  cnvtsr  18494  znleval  21491  ordtbas2  23106  ordtcnv  23116  ordtrest2  23119  cnconn  23337  tgqtop  23627  adj1o  31874  fcoinver  32584  fresf1o  32613  fcnvgreu  32655  dfcnv2  32658  preiman0  32691  gsumhashmul  33041  cycpmfvlem  33081  cycpmfv1  33082  cycpmfv2  33083  cycpmfv3  33084  cycpmrn  33112  cnvordtrestixx  33926  xrge0iifhmeo  33949  mbfmcst  34272  0rrv  34464  elrn3  35806  dfrn6  38350  cnvresrn  38390  dmxrn  38421  dmcoss2  38566  cnvrcl0  43728  conrel2d  43767  relexpaddss  43821  rntrclfvRP  43834  ntrneifv2  44183