Definition df-rn 4675

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 4674). For alternate definitions, see dfrn2 4855, dfrn3 4856, and dfrn4 5131. 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 4665	. 2 class ran 𝐴
3	1	ccnv 4663	. . 3 class ◡𝐴
4	3	cdm 4664	. 2 class dom ◡𝐴
5	2, 4	wceq 1364	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4855  dmcnvcnv  4891  rncnvcnv  4892  rneq  4894  rnss  4897  brelrng  4898  nfrn  4912  rncoss  4937  rncoeq  4940  cnvimarndm  5034  rnun  5079  rnin  5080  rnxpm  5100  rnxpss  5102  imainrect  5116  rnsnopg  5149  cnvssrndm  5192  cocnvss  5196  unidmrn  5203  dfdm2  5205  cnvexg  5208  fncnv  5325  funcnvres  5332  funimacnv  5335  fimacnvdisj  5445  dff1o4  5515  foimacnv  5525  funcocnv2  5532  f1ompt  5716  errn  6623  funrnfi  7017  sbthlemi5  7036  sbthlemi8  7039  sbthlemi9  7040  casefun  7160  caseinj  7164  djufun  7179  djuinj  7181  ctssdccl  7186  exmidfodomrlemim  7280  znleval  14285