Definition df-rn 5649

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 29447). Contrast with domain (defined in df-dm 5648). For alternate definitions, see dfrn2 5849, dfrn3 5850, and dfrn4 6159. 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 6028. Not to be confused with "codomain" (see df-f 6505), which may be a superset/superclass of the range (see frn 6680). (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 5639	. 2 class ran 𝐴
3	1	ccnv 5637	. . 3 class ◡𝐴
4	3	cdm 5638	. 2 class dom ◡𝐴
5	2, 4	wceq 1541	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5849  dmcnvcnv  5893  rncnvcnv  5894  rneq  5896  rnss  5899  brelrng  5901  nfrn  5912  rncoss  5932  rncoeq  5935  cnvimarndm  6039  rnun  6103  rnin  6104  rnxp  6127  rnxpss  6129  imainrect  6138  rnsnopg  6178  cnvssrndm  6228  unidmrn  6236  dfdm2  6238  funcnvpr  6568  funcnvtp  6569  funcnvqp  6570  fncnv  6579  funcnvres  6584  funimacnv  6587  fimacnvdisj  6725  dff1o4  6797  foimacnv  6806  funcocnv2  6814  f1ompt  7064  nvof1o  7231  cnvexg  7866  tz7.48-3  8395  errn  8677  omxpenlem  9024  sbthlem5  9038  sbthlem8  9041  sbthlem9  9042  fodomr  9079  domss2  9087  rnfi  9286  zorn2lem4  10444  rnct  10470  fpwwe2lem12  10587  trclublem  14892  relexpcnv  14932  relexpnnrn  14942  invf  17665  cicsym  17701  cnvtsr  18491  znleval  20998  ordtbas2  22579  ordtcnv  22589  ordtrest2  22592  cnconn  22810  tgqtop  23100  adj1o  30899  fcoinver  31592  fresf1o  31612  fcnvgreu  31656  dfcnv2  31659  preiman0  31691  gsumhashmul  31968  cycpmfvlem  32031  cycpmfv1  32032  cycpmfv2  32033  cycpmfv3  32034  cycpmrn  32062  cnvordtrestixx  32583  xrge0iifhmeo  32606  mbfmcst  32948  0rrv  33140  elrn3  34421  dfrn6  36836  cnvresrn  36882  dmcoss2  36989  cnvrcl0  42019  conrel2d  42058  relexpaddss  42112  rntrclfvRP  42125  ntrneifv2  42474