Definition df-rn 5600

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 28804). Contrast with domain (defined in df-dm 5599). For alternate definitions, see dfrn2 5797, dfrn3 5798, and dfrn4 6105. 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 5979. Not to be confused with "codomain" (see df-f 6437), which may be a superset/superclass of the range (see frn 6607). (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 5590	. 2 class ran 𝐴
3	1	ccnv 5588	. . 3 class ◡𝐴
4	3	cdm 5589	. 2 class dom ◡𝐴
5	2, 4	wceq 1539	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5797  dmcnvcnv  5842  rncnvcnv  5843  rneq  5845  rnss  5848  brelrng  5850  nfrn  5861  rncoss  5881  rncoeq  5884  cnvimarndm  5990  rnun  6049  rnin  6050  rnxp  6073  rnxpss  6075  imainrect  6084  rnsnopg  6124  cnvssrndm  6174  unidmrn  6182  dfdm2  6184  funcnvpr  6496  funcnvtp  6497  funcnvqp  6498  fncnv  6507  funcnvres  6512  funimacnv  6515  fimacnvdisj  6652  dff1o4  6724  foimacnv  6733  funcocnv2  6741  f1ompt  6985  nvof1o  7152  cnvexg  7771  tz7.48-3  8275  errn  8520  omxpenlem  8860  sbthlem5  8874  sbthlem8  8877  sbthlem9  8878  fodomr  8915  domss2  8923  rnfi  9102  zorn2lem4  10255  rnct  10281  fpwwe2lem12  10398  trclublem  14706  relexpcnv  14746  relexpnnrn  14756  invf  17480  cicsym  17516  cnvtsr  18306  znleval  20762  ordtbas2  22342  ordtcnv  22352  ordtrest2  22355  cnconn  22573  tgqtop  22863  adj1o  30256  fcoinver  30946  fresf1o  30966  fcnvgreu  31010  dfcnv2  31013  preiman0  31042  gsumhashmul  31316  cycpmfvlem  31379  cycpmfv1  31380  cycpmfv2  31381  cycpmfv3  31382  cycpmrn  31410  cnvordtrestixx  31863  xrge0iifhmeo  31886  mbfmcst  32226  0rrv  32418  elrn3  33729  dfrn6  36438  cnvresrn  36483  dmcoss2  36572  cnvrcl0  41233  conrel2d  41272  relexpaddss  41326  rntrclfvRP  41339  ntrneifv2  41690