Definition df-rn 5711

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30472). Contrast with domain (defined in df-dm 5710). For alternate definitions, see dfrn2 5913, dfrn3 5914, and dfrn4 6233. 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 6099. Not to be confused with "codomain" (see df-f 6577), which may be a superset/superclass of the range (see frn 6754). (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 5701	. 2 class ran 𝐴
3	1	ccnv 5699	. . 3 class ◡𝐴
4	3	cdm 5700	. 2 class dom ◡𝐴
5	2, 4	wceq 1537	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5913  dmcnvcnv  5958  rncnvcnv  5959  rneq  5961  rnss  5964  brelrng  5966  nfrn  5977  rncoss  5998  rncoeq  6002  cnvimarndm  6112  rnun  6177  rnin  6178  rnxp  6201  rnxpss  6203  imainrect  6212  rnsnopg  6252  cnvssrndm  6302  unidmrn  6310  dfdm2  6312  funcnvpr  6640  funcnvtp  6641  funcnvqp  6642  fncnv  6651  funcnvres  6656  funimacnv  6659  fimacnvdisj  6799  dff1o4  6870  foimacnv  6879  funcocnv2  6887  f1ompt  7145  nvof1o  7316  cnvexg  7964  tz7.48-3  8500  errn  8785  omxpenlem  9139  sbthlem5  9153  sbthlem8  9156  sbthlem9  9157  fodomr  9194  domss2  9202  fodomfir  9396  rnfi  9408  zorn2lem4  10568  rnct  10594  fpwwe2lem12  10711  trclublem  15044  relexpcnv  15084  relexpnnrn  15094  invf  17829  cicsym  17865  cnvtsr  18658  znleval  21596  ordtbas2  23220  ordtcnv  23230  ordtrest2  23233  cnconn  23451  tgqtop  23741  adj1o  31926  fcoinver  32626  fresf1o  32650  fcnvgreu  32691  dfcnv2  32694  preiman0  32721  gsumhashmul  33040  cycpmfvlem  33105  cycpmfv1  33106  cycpmfv2  33107  cycpmfv3  33108  cycpmrn  33136  cnvordtrestixx  33859  xrge0iifhmeo  33882  mbfmcst  34224  0rrv  34416  elrn3  35724  dfrn6  38258  cnvresrn  38304  dmcoss2  38410  cnvrcl0  43587  conrel2d  43626  relexpaddss  43680  rntrclfvRP  43693  ntrneifv2  44042