Definition df-rn 4787

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 4786). For alternate definitions, see dfrn2 4970, dfrn3 4971, and dfrn4 5251. 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 4777	. 2 class ran 𝐴
3	1	ccnv 4775	. . 3 class ◡𝐴
4	3	cdm 4776	. 2 class dom ◡𝐴
5	2, 4	wceq 1402	1 wff ran 𝐴 = dom ◡𝐴

This definition is used by:  dfrn2  4970  dmcnvcnv  5008  rncnvcnv  5009  rneq  5011  rnss  5014  brelrng  5015  nfrn  5029  rncoss  5055  rncoeq  5058  cnvimarndm  5154  rnun  5199  rnin  5200  rnxpm  5220  rnxpss  5222  imainrect  5236  rnsnopg  5269  cnvssrndm  5312  cocnvss  5316  unidmrn  5323  dfdm2  5325  cnvexg  5328  fncnv  5450  funcnvres  5457  funimacnv  5460  fimacnvdisj  5579  dff1o4  5650  foimacnv  5660  funcocnv2  5667  f1ompt  5862  errn  6833  funrnfi  7260  sbthlemi5  7283  sbthlemi8  7286  sbthlemi9  7287  casefun  7431  caseinj  7435  djufun  7450  djuinj  7452  ctssdccl  7457  exmidfodomrlemim  7559  znleval  15097