Definition df-rn 4734

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 4733). For alternate definitions, see dfrn2 4916, dfrn3 4917, and dfrn4 5195. 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 4724	. 2 class ran 𝐴
3	1	ccnv 4722	. . 3 class ◡𝐴
4	3	cdm 4723	. 2 class dom ◡𝐴
5	2, 4	wceq 1395	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4916  dmcnvcnv  4954  rncnvcnv  4955  rneq  4957  rnss  4960  brelrng  4961  nfrn  4975  rncoss  5001  rncoeq  5004  cnvimarndm  5098  rnun  5143  rnin  5144  rnxpm  5164  rnxpss  5166  imainrect  5180  rnsnopg  5213  cnvssrndm  5256  cocnvss  5260  unidmrn  5267  dfdm2  5269  cnvexg  5272  fncnv  5393  funcnvres  5400  funimacnv  5403  fimacnvdisj  5518  dff1o4  5588  foimacnv  5598  funcocnv2  5605  f1ompt  5794  errn  6719  funrnfi  7132  sbthlemi5  7151  sbthlemi8  7154  sbthlemi9  7155  casefun  7275  caseinj  7279  djufun  7294  djuinj  7296  ctssdccl  7301  exmidfodomrlemim  7402  znleval  14657