Definition df-rn 5642

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30342). Contrast with domain (defined in df-dm 5641). For alternate definitions, see dfrn2 5842, dfrn3 5843, and dfrn4 6163. 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 6030. Not to be confused with "codomain" (see df-f 6503), which may be a superset/superclass of the range (see frn 6677). (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 5632	. 2 class ran 𝐴
3	1	ccnv 5630	. . 3 class ◡𝐴
4	3	cdm 5631	. 2 class dom ◡𝐴
5	2, 4	wceq 1540	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5842  dmcnvcnv  5886  rncnvcnv  5887  rneq  5889  rnss  5892  brelrng  5894  nfrn  5905  rncoss  5928  rncoeq  5932  cnvimarndm  6043  rnun  6106  rnin  6107  rnxp  6131  rnxpss  6133  imainrect  6142  rnsnopg  6182  cnvssrndm  6232  unidmrn  6240  dfdm2  6242  funcnvpr  6562  funcnvtp  6563  funcnvqp  6564  fncnv  6573  funcnvres  6578  funimacnv  6581  fimacnvdisj  6720  dff1o4  6790  foimacnv  6799  funcocnv2  6807  f1ompt  7065  nvof1o  7237  cnvexg  7880  tz7.48-3  8389  errn  8670  omxpenlem  9019  sbthlem5  9032  sbthlem8  9035  sbthlem9  9036  fodomr  9069  domss2  9077  fodomfir  9255  rnfi  9267  zorn2lem4  10428  rnct  10454  fpwwe2lem12  10571  trclublem  14937  relexpcnv  14977  relexpnnrn  14987  invf  17706  cicsym  17742  cnvtsr  18523  znleval  21440  ordtbas2  23054  ordtcnv  23064  ordtrest2  23067  cnconn  23285  tgqtop  23575  adj1o  31796  fcoinver  32506  fresf1o  32528  fcnvgreu  32570  dfcnv2  32573  preiman0  32606  gsumhashmul  32974  cycpmfvlem  33042  cycpmfv1  33043  cycpmfv2  33044  cycpmfv3  33045  cycpmrn  33073  cnvordtrestixx  33876  xrge0iifhmeo  33899  mbfmcst  34223  0rrv  34415  elrn3  35722  dfrn6  38263  cnvresrn  38303  dmxrn  38333  dmcoss2  38418  cnvrcl0  43587  conrel2d  43626  relexpaddss  43680  rntrclfvRP  43693  ntrneifv2  44042