Definition df-rn 5624

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30371). Contrast with domain (defined in df-dm 5623). For alternate definitions, see dfrn2 5825, dfrn3 5826, and dfrn4 6145. 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 6015. Not to be confused with "codomain" (see df-f 6480), which may be a superset/superclass of the range (see frn 6653). (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 5614	. 2 class ran 𝐴
3	1	ccnv 5612	. . 3 class ◡𝐴
4	3	cdm 5613	. 2 class dom ◡𝐴
5	2, 4	wceq 1540	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5825  dmcnvcnv  5869  rncnvcnv  5870  rneq  5872  rnss  5875  brelrng  5877  nfrn  5888  rncoss  5912  rncoeq  5917  cnvimarndm  6028  rnun  6088  rnin  6089  rnxp  6113  rnxpss  6115  imainrect  6124  rnsnopg  6164  cnvssrndm  6213  unidmrn  6221  dfdm2  6223  funcnvpr  6538  funcnvtp  6539  funcnvqp  6540  fncnv  6549  funcnvres  6554  funimacnv  6557  fimacnvdisj  6696  dff1o4  6766  foimacnv  6775  funcocnv2  6783  f1ompt  7038  nvof1o  7208  cnvexg  7848  tz7.48-3  8357  errn  8638  omxpenlem  8985  sbthlem5  8998  sbthlem8  9001  sbthlem9  9002  fodomr  9035  domss2  9043  fodomfir  9206  rnfi  9218  zorn2lem4  10381  rnct  10407  fpwwe2lem12  10524  trclublem  14889  relexpcnv  14929  relexpnnrn  14939  invf  17662  cicsym  17698  cnvtsr  18481  znleval  21445  ordtbas2  23060  ordtcnv  23070  ordtrest2  23073  cnconn  23291  tgqtop  23581  adj1o  31825  fcoinver  32536  fresf1o  32565  fcnvgreu  32607  dfcnv2  32610  preiman0  32643  gsumhashmul  33009  cycpmfvlem  33049  cycpmfv1  33050  cycpmfv2  33051  cycpmfv3  33052  cycpmrn  33080  cnvordtrestixx  33894  xrge0iifhmeo  33917  mbfmcst  34240  0rrv  34432  elrn3  35752  dfrn6  38293  cnvresrn  38333  dmxrn  38363  dmcoss2  38448  cnvrcl0  43615  conrel2d  43654  relexpaddss  43708  rntrclfvRP  43721  ntrneifv2  44070