Definition df-rn 4694

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 4693). For alternate definitions, see dfrn2 4874, dfrn3 4875, and dfrn4 5152. 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 4684	. 2 class ran 𝐴
3	1	ccnv 4682	. . 3 class ◡𝐴
4	3	cdm 4683	. 2 class dom ◡𝐴
5	2, 4	wceq 1373	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4874  dmcnvcnv  4911  rncnvcnv  4912  rneq  4914  rnss  4917  brelrng  4918  nfrn  4932  rncoss  4958  rncoeq  4961  cnvimarndm  5055  rnun  5100  rnin  5101  rnxpm  5121  rnxpss  5123  imainrect  5137  rnsnopg  5170  cnvssrndm  5213  cocnvss  5217  unidmrn  5224  dfdm2  5226  cnvexg  5229  fncnv  5349  funcnvres  5356  funimacnv  5359  fimacnvdisj  5472  dff1o4  5542  foimacnv  5552  funcocnv2  5559  f1ompt  5744  errn  6655  funrnfi  7059  sbthlemi5  7078  sbthlemi8  7081  sbthlemi9  7082  casefun  7202  caseinj  7206  djufun  7221  djuinj  7223  ctssdccl  7228  exmidfodomrlemim  7325  znleval  14490