Definition df-rn 4609

Description: Define the range of a class. For example, F = { ⟨ 2 , 6 ⟩, ⟨ 3 , 9 ⟩ } -> ran F = { 6 , 9 } . Contrast with domain (defined in df-dm 4608). For alternate definitions, see dfrn2 4786, dfrn3 4787, and dfrn4 5058. The notation "ran " is used by Enderton; other authors sometimes use script R or script W. (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 4599	. 2 class ran 𝐴
3	1	ccnv 4597	. . 3 class ◡𝐴
4	3	cdm 4598	. 2 class dom ◡𝐴
5	2, 4	wceq 1342	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4786  dmcnvcnv  4822  rncnvcnv  4823  rneq  4825  rnss  4828  brelrng  4829  nfrn  4843  rncoss  4868  rncoeq  4871  cnvimarndm  4962  rnun  5006  rnin  5007  rnxpm  5027  rnxpss  5029  imainrect  5043  rnsnopg  5076  cnvssrndm  5119  cocnvss  5123  unidmrn  5130  dfdm2  5132  cnvexg  5135  fncnv  5248  funcnvres  5255  funimacnv  5258  fimacnvdisj  5366  dff1o4  5434  foimacnv  5444  funcocnv2  5451  f1ompt  5630  errn  6514  funrnfi  6898  sbthlemi5  6917  sbthlemi8  6920  sbthlemi9  6921  casefun  7041  caseinj  7045  djufun  7060  djuinj  7062  ctssdccl  7067  exmidfodomrlemim  7148