Definition df-rn 5688

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 29693). Contrast with domain (defined in df-dm 5687). For alternate definitions, see dfrn2 5889, dfrn3 5890, and dfrn4 6202. 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 6070. Not to be confused with "codomain" (see df-f 6548), which may be a superset/superclass of the range (see frn 6725). (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 5678	. 2 class ran 𝐴
3	1	ccnv 5676	. . 3 class ◡𝐴
4	3	cdm 5677	. 2 class dom ◡𝐴
5	2, 4	wceq 1542	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5889  dmcnvcnv  5933  rncnvcnv  5934  rneq  5936  rnss  5939  brelrng  5941  nfrn  5952  rncoss  5972  rncoeq  5975  cnvimarndm  6082  rnun  6146  rnin  6147  rnxp  6170  rnxpss  6172  imainrect  6181  rnsnopg  6221  cnvssrndm  6271  unidmrn  6279  dfdm2  6281  funcnvpr  6611  funcnvtp  6612  funcnvqp  6613  fncnv  6622  funcnvres  6627  funimacnv  6630  fimacnvdisj  6770  dff1o4  6842  foimacnv  6851  funcocnv2  6859  f1ompt  7111  nvof1o  7278  cnvexg  7915  tz7.48-3  8444  errn  8725  omxpenlem  9073  sbthlem5  9087  sbthlem8  9090  sbthlem9  9091  fodomr  9128  domss2  9136  rnfi  9335  zorn2lem4  10494  rnct  10520  fpwwe2lem12  10637  trclublem  14942  relexpcnv  14982  relexpnnrn  14992  invf  17715  cicsym  17751  cnvtsr  18541  znleval  21110  ordtbas2  22695  ordtcnv  22705  ordtrest2  22708  cnconn  22926  tgqtop  23216  adj1o  31147  fcoinver  31835  fresf1o  31855  fcnvgreu  31898  dfcnv2  31901  preiman0  31931  gsumhashmul  32208  cycpmfvlem  32271  cycpmfv1  32272  cycpmfv2  32273  cycpmfv3  32274  cycpmrn  32302  cnvordtrestixx  32893  xrge0iifhmeo  32916  mbfmcst  33258  0rrv  33450  elrn3  34732  dfrn6  37171  cnvresrn  37217  dmcoss2  37324  cnvrcl0  42376  conrel2d  42415  relexpaddss  42469  rntrclfvRP  42482  ntrneifv2  42831