Definition df-rn 5665

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30367). Contrast with domain (defined in df-dm 5664). For alternate definitions, see dfrn2 5868, dfrn3 5869, and dfrn4 6191. 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 6057. Not to be confused with "codomain" (see df-f 6534), which may be a superset/superclass of the range (see frn 6712). (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 5655	. 2 class ran 𝐴
3	1	ccnv 5653	. . 3 class ◡𝐴
4	3	cdm 5654	. 2 class dom ◡𝐴
5	2, 4	wceq 1540	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5868  dmcnvcnv  5913  rncnvcnv  5914  rneq  5916  rnss  5919  brelrng  5921  nfrn  5932  rncoss  5955  rncoeq  5959  cnvimarndm  6070  rnun  6134  rnin  6135  rnxp  6159  rnxpss  6161  imainrect  6170  rnsnopg  6210  cnvssrndm  6260  unidmrn  6268  dfdm2  6270  funcnvpr  6597  funcnvtp  6598  funcnvqp  6599  fncnv  6608  funcnvres  6613  funimacnv  6616  fimacnvdisj  6755  dff1o4  6825  foimacnv  6834  funcocnv2  6842  f1ompt  7100  nvof1o  7272  cnvexg  7918  tz7.48-3  8456  errn  8739  omxpenlem  9085  sbthlem5  9099  sbthlem8  9102  sbthlem9  9103  fodomr  9140  domss2  9148  fodomfir  9338  rnfi  9350  zorn2lem4  10511  rnct  10537  fpwwe2lem12  10654  trclublem  15012  relexpcnv  15052  relexpnnrn  15062  invf  17779  cicsym  17815  cnvtsr  18596  znleval  21513  ordtbas2  23127  ordtcnv  23137  ordtrest2  23140  cnconn  23358  tgqtop  23648  adj1o  31821  fcoinver  32531  fresf1o  32555  fcnvgreu  32597  dfcnv2  32600  preiman0  32633  gsumhashmul  33001  cycpmfvlem  33069  cycpmfv1  33070  cycpmfv2  33071  cycpmfv3  33072  cycpmrn  33100  cnvordtrestixx  33890  xrge0iifhmeo  33913  mbfmcst  34237  0rrv  34429  elrn3  35725  dfrn6  38266  cnvresrn  38312  dmcoss2  38418  cnvrcl0  43596  conrel2d  43635  relexpaddss  43689  rntrclfvRP  43702  ntrneifv2  44051