Definition df-rn 5636

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30519). Contrast with domain (defined in df-dm 5635). For alternate definitions, see dfrn2 5838, dfrn3 5839, and dfrn4 6161. 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 6030. Not to be confused with "codomain" (see df-f 6497), which may be a superset/superclass of the range (see frn 6670). (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 5626	. 2 class ran 𝐴
3	1	ccnv 5624	. . 3 class ◡𝐴
4	3	cdm 5625	. 2 class dom ◡𝐴
5	2, 4	wceq 1542	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5838  dmcnvcnv  5883  rncnvcnv  5884  rneq  5886  rnss  5889  brelrng  5891  nfrn  5902  rncoss  5927  rncoeq  5932  cnvimarndm  6043  rnun  6104  rnin  6105  rnxp  6129  rnxpss  6131  imainrect  6140  rnsnopg  6180  cnvssrndm  6230  unidmrn  6238  dfdm2  6240  funcnvpr  6555  funcnvtp  6556  funcnvqp  6557  fncnv  6566  funcnvres  6571  funimacnv  6574  fimacnvdisj  6713  dff1o4  6783  foimacnv  6792  funcocnv2  6800  f1ompt  7058  nvof1o  7228  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  10413  rnct  10439  fpwwe2lem12  10557  trclublem  14922  relexpcnv  14962  relexpnnrn  14972  invf  17696  cicsym  17732  cnvtsr  18515  znleval  21513  ordtbas2  23139  ordtcnv  23149  ordtrest2  23152  cnconn  23370  tgqtop  23660  adj1o  31973  fcoinver  32682  fresf1o  32712  fcnvgreu  32753  dfcnv2  32756  preiman0  32791  gsumhashmul  33152  cycpmfvlem  33196  cycpmfv1  33197  cycpmfv2  33198  cycpmfv3  33199  cycpmrn  33227  cnvordtrestixx  34072  xrge0iifhmeo  34095  mbfmcst  34418  0rrv  34610  elrn3  35958  dfrn6  38511  cnvresrn  38551  dmxrn  38590  dmcoss2  38747  cnvrcl0  43933  conrel2d  43972  relexpaddss  44026  rntrclfvRP  44039  ntrneifv2  44388