Definition df-rn 4639

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 4638). For alternate definitions, see dfrn2 4817, dfrn3 4818, and dfrn4 5091. 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 4629	. 2 class ran 𝐴
3	1	ccnv 4627	. . 3 class ◡𝐴
4	3	cdm 4628	. 2 class dom ◡𝐴
5	2, 4	wceq 1353	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4817  dmcnvcnv  4853  rncnvcnv  4854  rneq  4856  rnss  4859  brelrng  4860  nfrn  4874  rncoss  4899  rncoeq  4902  cnvimarndm  4994  rnun  5039  rnin  5040  rnxpm  5060  rnxpss  5062  imainrect  5076  rnsnopg  5109  cnvssrndm  5152  cocnvss  5156  unidmrn  5163  dfdm2  5165  cnvexg  5168  fncnv  5284  funcnvres  5291  funimacnv  5294  fimacnvdisj  5402  dff1o4  5471  foimacnv  5481  funcocnv2  5488  f1ompt  5669  errn  6559  funrnfi  6943  sbthlemi5  6962  sbthlemi8  6965  sbthlemi9  6966  casefun  7086  caseinj  7090  djufun  7105  djuinj  7107  ctssdccl  7112  exmidfodomrlemim  7202