Definition df-rn 4684

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 4683). For alternate definitions, see dfrn2 4864, dfrn3 4865, and dfrn4 5140. 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 4674	. 2 class ran 𝐴
3	1	ccnv 4672	. . 3 class ◡𝐴
4	3	cdm 4673	. 2 class dom ◡𝐴
5	2, 4	wceq 1372	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4864  dmcnvcnv  4900  rncnvcnv  4901  rneq  4903  rnss  4906  brelrng  4907  nfrn  4921  rncoss  4946  rncoeq  4949  cnvimarndm  5043  rnun  5088  rnin  5089  rnxpm  5109  rnxpss  5111  imainrect  5125  rnsnopg  5158  cnvssrndm  5201  cocnvss  5205  unidmrn  5212  dfdm2  5214  cnvexg  5217  fncnv  5334  funcnvres  5341  funimacnv  5344  fimacnvdisj  5454  dff1o4  5524  foimacnv  5534  funcocnv2  5541  f1ompt  5725  errn  6632  funrnfi  7026  sbthlemi5  7045  sbthlemi8  7048  sbthlemi9  7049  casefun  7169  caseinj  7173  djufun  7188  djuinj  7190  ctssdccl  7195  exmidfodomrlemim  7291  znleval  14333