Definition df-rn 5672

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30757). Contrast with domain (defined in df-dm 5671). For alternate definitions, see dfrn2 5878, dfrn3 5879, and dfrn4 6201. 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 6072. Not to be confused with "codomain" (see df-f 6540), which may be a superset/superclass of the range (see frn 6713). (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 5662	. 2 class ran 𝐴
3	1	ccnv 5660	. . 3 class ◡𝐴
4	3	cdm 5661	. 2 class dom ◡𝐴
5	2, 4	wceq 1568	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5878  dmcnvcnv  5923  rncnvcnv  5924  rneq  5926  rnss  5929  brelrng  5931  nfrn  5942  rncoss  5967  rncoeq  5971  cnvimarndm  6085  rnun  6142  rninOLD  6144  rnxp  6168  rnxpss  6170  imainrect  6179  rnsnopg  6222  cnvssrndm  6272  unidmrn  6280  dfdm2  6282  funcnvpr  6598  funcnvtp  6599  funcnvqp  6600  fncnv  6609  funcnvres  6614  funimacnv  6617  fimacnvdisj  6756  dff1o4  6829  foimacnv  6838  funcocnv2  6846  f1ompt  7106  nvof1o  7278  cnvexg  7920  tz7.48-3  8430  errn  8716  omxpenlem  9065  sbthlem5  9078  sbthlem8  9081  sbthlem9  9082  fodomr  9115  domss2  9123  fodomfir  9286  rnfi  9296  zorn2lem4  10482  rnct  10508  fpwwe2lem12  10626  trclublem  15031  relexpcnv  15071  relexpnnrn  15081  invf  17824  cicsym  17860  cnvtsr  18643  znleval  21683  ordtbas2  23327  ordtcnv  23337  ordtrest2  23340  cnconn  23558  tgqtop  23848  adj1o  32212  fcoinver  32915  fresf1o  32942  fcnvgreu  32983  dfcnv2  32986  preiman0  33021  gsumhashmul  33353  cycpmfvlem  33398  cycpmfv1  33399  cycpmfv2  33400  cycpmfv3  33401  cycpmrn  33429  cnvordtrestixx  34269  xrge0iifhmeo  34292  mbfmcst  34615  0rrv  34807  elrn3  36208  dfrn6  38903  cnvresrn  38943  dmxrn  38982  dmcoss2  39139  cnvrcl0  44299  conrel2d  44338  relexpaddss  44392  rntrclfvRP  44405  ntrneifv2  44754