Definition df-rn 4670

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 4669). For alternate definitions, see dfrn2 4850, dfrn3 4851, and dfrn4 5126. 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 4660	. 2 class ran 𝐴
3	1	ccnv 4658	. . 3 class ◡𝐴
4	3	cdm 4659	. 2 class dom ◡𝐴
5	2, 4	wceq 1364	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4850  dmcnvcnv  4886  rncnvcnv  4887  rneq  4889  rnss  4892  brelrng  4893  nfrn  4907  rncoss  4932  rncoeq  4935  cnvimarndm  5029  rnun  5074  rnin  5075  rnxpm  5095  rnxpss  5097  imainrect  5111  rnsnopg  5144  cnvssrndm  5187  cocnvss  5191  unidmrn  5198  dfdm2  5200  cnvexg  5203  fncnv  5320  funcnvres  5327  funimacnv  5330  fimacnvdisj  5438  dff1o4  5508  foimacnv  5518  funcocnv2  5525  f1ompt  5709  errn  6609  funrnfi  7001  sbthlemi5  7020  sbthlemi8  7023  sbthlemi9  7024  casefun  7144  caseinj  7148  djufun  7163  djuinj  7165  ctssdccl  7170  exmidfodomrlemim  7261  znleval  14141