Definition df-rn 4550

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 4549). For alternate definitions, see dfrn2 4727, dfrn3 4728, and dfrn4 4999. 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 4540	. 2 class ran 𝐴
3	1	ccnv 4538	. . 3 class ◡𝐴
4	3	cdm 4539	. 2 class dom ◡𝐴
5	2, 4	wceq 1331	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4727  dmcnvcnv  4763  rncnvcnv  4764  rneq  4766  rnss  4769  brelrng  4770  nfrn  4784  rncoss  4809  rncoeq  4812  cnvimarndm  4903  rnun  4947  rnin  4948  rnxpm  4968  rnxpss  4970  imainrect  4984  rnsnopg  5017  cnvssrndm  5060  cocnvss  5064  unidmrn  5071  dfdm2  5073  cnvexg  5076  fncnv  5189  funcnvres  5196  funimacnv  5199  fimacnvdisj  5307  dff1o4  5375  foimacnv  5385  funcocnv2  5392  f1ompt  5571  errn  6451  funrnfi  6830  sbthlemi5  6849  sbthlemi8  6852  sbthlemi9  6853  casefun  6970  caseinj  6974  djufun  6989  djuinj  6991  ctssdccl  6996  exmidfodomrlemim  7057