Definition df-rn 5689

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30322). Contrast with domain (defined in df-dm 5688). For alternate definitions, see dfrn2 5891, dfrn3 5892, and dfrn4 6208. 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 6074. Not to be confused with "codomain" (see df-f 6553), which may be a superset/superclass of the range (see frn 6730). (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 5679	. 2 class ran 𝐴
3	1	ccnv 5677	. . 3 class ◡𝐴
4	3	cdm 5678	. 2 class dom ◡𝐴
5	2, 4	wceq 1533	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5891  dmcnvcnv  5935  rncnvcnv  5936  rneq  5938  rnss  5941  brelrng  5943  nfrn  5954  rncoss  5975  rncoeq  5978  cnvimarndm  6087  rnun  6152  rnin  6153  rnxp  6176  rnxpss  6178  imainrect  6187  rnsnopg  6227  cnvssrndm  6277  unidmrn  6285  dfdm2  6287  funcnvpr  6616  funcnvtp  6617  funcnvqp  6618  fncnv  6627  funcnvres  6632  funimacnv  6635  fimacnvdisj  6775  dff1o4  6846  foimacnv  6855  funcocnv2  6863  f1ompt  7120  nvof1o  7289  cnvexg  7932  tz7.48-3  8465  errn  8747  omxpenlem  9098  sbthlem5  9112  sbthlem8  9115  sbthlem9  9116  fodomr  9153  domss2  9161  rnfi  9361  zorn2lem4  10524  rnct  10550  fpwwe2lem12  10667  trclublem  14978  relexpcnv  15018  relexpnnrn  15028  invf  17754  cicsym  17790  cnvtsr  18583  znleval  21505  ordtbas2  23139  ordtcnv  23149  ordtrest2  23152  cnconn  23370  tgqtop  23660  adj1o  31776  fcoinver  32473  fresf1o  32497  fcnvgreu  32540  dfcnv2  32543  preiman0  32571  gsumhashmul  32860  cycpmfvlem  32925  cycpmfv1  32926  cycpmfv2  32927  cycpmfv3  32928  cycpmrn  32956  cnvordtrestixx  33645  xrge0iifhmeo  33668  mbfmcst  34010  0rrv  34202  elrn3  35487  dfrn6  37904  cnvresrn  37950  dmcoss2  38056  cnvrcl0  43197  conrel2d  43236  relexpaddss  43290  rntrclfvRP  43303  ntrneifv2  43652