Definition df-rn 5590

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 28680). Contrast with domain (defined in df-dm 5589). For alternate definitions, see dfrn2 5785, dfrn3 5786, and dfrn4 6093. 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 5967. Not to be confused with "codomain" (see df-f 6419), which may be a superset/superclass of the range (see frn 6588). (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 5580	. 2 class ran 𝐴
3	1	ccnv 5578	. . 3 class ◡𝐴
4	3	cdm 5579	. 2 class dom ◡𝐴
5	2, 4	wceq 1543	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5785  dmcnvcnv  5830  rncnvcnv  5831  rneq  5833  rnss  5836  brelrng  5838  nfrn  5849  rncoss  5869  rncoeq  5872  cnvimarndm  5978  rnun  6037  rnin  6038  rnxp  6061  rnxpss  6063  imainrect  6072  rnsnopg  6112  cnvssrndm  6162  unidmrn  6170  dfdm2  6172  funcnvpr  6477  funcnvtp  6478  funcnvqp  6479  fncnv  6488  funcnvres  6493  funimacnv  6496  fimacnvdisj  6633  dff1o4  6705  foimacnv  6714  funcocnv2  6721  f1ompt  6964  nvof1o  7130  cnvexg  7742  tz7.48-3  8222  errn  8455  omxpenlem  8790  sbthlem5  8804  sbthlem8  8807  sbthlem9  8808  fodomr  8841  domss2  8849  rnfi  9007  zorn2lem4  10161  rnct  10187  fpwwe2lem12  10304  trclublem  14609  relexpcnv  14649  relexpnnrn  14659  invf  17372  cicsym  17408  cnvtsr  18196  znleval  20649  ordtbas2  22225  ordtcnv  22235  ordtrest2  22238  cnconn  22456  tgqtop  22746  adj1o  30132  fcoinver  30822  fresf1o  30842  fcnvgreu  30887  dfcnv2  30890  preiman0  30919  gsumhashmul  31193  cycpmfvlem  31256  cycpmfv1  31257  cycpmfv2  31258  cycpmfv3  31259  cycpmrn  31287  cnvordtrestixx  31740  xrge0iifhmeo  31763  mbfmcst  32101  0rrv  32293  elrn3  33610  dfrn6  36344  cnvresrn  36389  dmcoss2  36478  cnvrcl0  41094  conrel2d  41134  relexpaddss  41188  rntrclfvRP  41201  ntrneifv2  41552