Definition df-rn 5630

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30384). Contrast with domain (defined in df-dm 5629). For alternate definitions, see dfrn2 5831, dfrn3 5832, and dfrn4 6151. 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 6021. Not to be confused with "codomain" (see df-f 6486), which may be a superset/superclass of the range (see frn 6659). (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 5620	. 2 class ran 𝐴
3	1	ccnv 5618	. . 3 class ◡𝐴
4	3	cdm 5619	. 2 class dom ◡𝐴
5	2, 4	wceq 1540	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5831  dmcnvcnv  5875  rncnvcnv  5876  rneq  5878  rnss  5881  brelrng  5883  nfrn  5894  rncoss  5918  rncoeq  5923  cnvimarndm  6034  rnun  6094  rnin  6095  rnxp  6119  rnxpss  6121  imainrect  6130  rnsnopg  6170  cnvssrndm  6219  unidmrn  6227  dfdm2  6229  funcnvpr  6544  funcnvtp  6545  funcnvqp  6546  fncnv  6555  funcnvres  6560  funimacnv  6563  fimacnvdisj  6702  dff1o4  6772  foimacnv  6781  funcocnv2  6789  f1ompt  7045  nvof1o  7217  cnvexg  7857  tz7.48-3  8366  errn  8647  omxpenlem  8995  sbthlem5  9008  sbthlem8  9011  sbthlem9  9012  fodomr  9045  domss2  9053  fodomfir  9218  rnfi  9230  zorn2lem4  10393  rnct  10419  fpwwe2lem12  10536  trclublem  14902  relexpcnv  14942  relexpnnrn  14952  invf  17675  cicsym  17711  cnvtsr  18494  znleval  21461  ordtbas2  23076  ordtcnv  23086  ordtrest2  23089  cnconn  23307  tgqtop  23597  adj1o  31838  fcoinver  32548  fresf1o  32575  fcnvgreu  32617  dfcnv2  32620  preiman0  32653  gsumhashmul  33015  cycpmfvlem  33055  cycpmfv1  33056  cycpmfv2  33057  cycpmfv3  33058  cycpmrn  33086  cnvordtrestixx  33886  xrge0iifhmeo  33909  mbfmcst  34233  0rrv  34425  elrn3  35745  dfrn6  38286  cnvresrn  38326  dmxrn  38356  dmcoss2  38441  cnvrcl0  43608  conrel2d  43647  relexpaddss  43701  rntrclfvRP  43714  ntrneifv2  44063