Definition df-rn 5649

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30369). Contrast with domain (defined in df-dm 5648). For alternate definitions, see dfrn2 5852, dfrn3 5853, and dfrn4 6175. 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 6041. Not to be confused with "codomain" (see df-f 6515), which may be a superset/superclass of the range (see frn 6695). (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 1540	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5852  dmcnvcnv  5897  rncnvcnv  5898  rneq  5900  rnss  5903  brelrng  5905  nfrn  5916  rncoss  5939  rncoeq  5943  cnvimarndm  6054  rnun  6118  rnin  6119  rnxp  6143  rnxpss  6145  imainrect  6154  rnsnopg  6194  cnvssrndm  6244  unidmrn  6252  dfdm2  6254  funcnvpr  6578  funcnvtp  6579  funcnvqp  6580  fncnv  6589  funcnvres  6594  funimacnv  6597  fimacnvdisj  6738  dff1o4  6808  foimacnv  6817  funcocnv2  6825  f1ompt  7083  nvof1o  7255  cnvexg  7900  tz7.48-3  8412  errn  8693  omxpenlem  9042  sbthlem5  9055  sbthlem8  9058  sbthlem9  9059  fodomr  9092  domss2  9100  fodomfir  9279  rnfi  9291  zorn2lem4  10452  rnct  10478  fpwwe2lem12  10595  trclublem  14961  relexpcnv  15001  relexpnnrn  15011  invf  17730  cicsym  17766  cnvtsr  18547  znleval  21464  ordtbas2  23078  ordtcnv  23088  ordtrest2  23091  cnconn  23309  tgqtop  23599  adj1o  31823  fcoinver  32533  fresf1o  32555  fcnvgreu  32597  dfcnv2  32600  preiman0  32633  gsumhashmul  33001  cycpmfvlem  33069  cycpmfv1  33070  cycpmfv2  33071  cycpmfv3  33072  cycpmrn  33100  cnvordtrestixx  33903  xrge0iifhmeo  33926  mbfmcst  34250  0rrv  34442  elrn3  35749  dfrn6  38290  cnvresrn  38330  dmxrn  38360  dmcoss2  38445  cnvrcl0  43614  conrel2d  43653  relexpaddss  43707  rntrclfvRP  43720  ntrneifv2  44069