Definition df-rn 4374

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 4373). For alternate definitions, see dfrn2 4541, dfrn3 4542, and dfrn4 4801. 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 4364	. 2 class ran 𝐴
3	1	ccnv 4362	. . 3 class ◡𝐴
4	3	cdm 4363	. 2 class dom ◡𝐴
5	2, 4	wceq 1284	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4541  dmcnvcnv  4576  rncnvcnv  4577  rneq  4579  rnss  4582  brelrng  4583  nfrn  4597  rncoss  4620  rncoeq  4623  cnvimarndm  4709  rnun  4752  rnin  4753  rnxpm  4772  rnxpss  4774  imainrect  4786  rnsnopg  4819  cnvssrndm  4862  unidmrn  4870  dfdm2  4872  cnvexg  4875  fncnv  4985  funcnvres  4992  funimacnv  4995  fimacnvdisj  5094  dff1o4  5154  foimacnv  5164  funcocnv2  5171  f1ompt  5341  errn  6151  funrnfi  6392