Definition df-rn 5660

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30644). Contrast with domain (defined in df-dm 5659). For alternate definitions, see dfrn2 5866, dfrn3 5867, and dfrn4 6191. 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 6061. Not to be confused with "codomain" (see df-f 6527), which may be a superset/superclass of the range (see frn 6701). (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 5650	. 2 class ran 𝐴
3	1	ccnv 5648	. . 3 class ◡𝐴
4	3	cdm 5649	. 2 class dom ◡𝐴
5	2, 4	wceq 1562	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5866  dmcnvcnv  5911  rncnvcnv  5912  rneq  5914  rnss  5917  brelrng  5919  nfrn  5930  rncoss  5955  rncoeq  5960  cnvimarndm  6074  rnun  6131  rninOLD  6133  rnxp  6158  rnxpss  6160  imainrect  6169  rnsnopg  6210  cnvssrndm  6260  unidmrn  6268  dfdm2  6270  funcnvpr  6585  funcnvtp  6586  funcnvqp  6587  fncnv  6596  funcnvres  6601  funimacnv  6604  fimacnvdisj  6744  dff1o4  6817  foimacnv  6826  funcocnv2  6834  f1ompt  7094  nvof1o  7266  cnvexg  7907  tz7.48-3  8417  errn  8703  omxpenlem  9052  sbthlem5  9065  sbthlem8  9068  sbthlem9  9069  fodomr  9102  domss2  9110  fodomfir  9274  rnfi  9285  zorn2lem4  10458  rnct  10484  fpwwe2lem12  10602  trclublem  15010  relexpcnv  15050  relexpnnrn  15060  invf  17803  cicsym  17839  cnvtsr  18622  znleval  21608  ordtbas2  23253  ordtcnv  23263  ordtrest2  23266  cnconn  23484  tgqtop  23774  adj1o  32099  fcoinver  32806  fresf1o  32835  fcnvgreu  32876  dfcnv2  32879  preiman0  32914  gsumhashmul  33249  cycpmfvlem  33294  cycpmfv1  33295  cycpmfv2  33296  cycpmfv3  33297  cycpmrn  33325  cnvordtrestixx  34212  xrge0iifhmeo  34235  mbfmcst  34558  0rrv  34750  elrn3  36117  dfrn6  38812  cnvresrn  38852  dmxrn  38891  dmcoss2  39048  cnvrcl0  44206  conrel2d  44245  relexpaddss  44299  rntrclfvRP  44312  ntrneifv2  44661