Definition df-rn 4730

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 4729). For alternate definitions, see dfrn2 4910, dfrn3 4911, and dfrn4 5189. 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 4720	. 2 class ran 𝐴
3	1	ccnv 4718	. . 3 class ◡𝐴
4	3	cdm 4719	. 2 class dom ◡𝐴
5	2, 4	wceq 1395	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4910  dmcnvcnv  4948  rncnvcnv  4949  rneq  4951  rnss  4954  brelrng  4955  nfrn  4969  rncoss  4995  rncoeq  4998  cnvimarndm  5092  rnun  5137  rnin  5138  rnxpm  5158  rnxpss  5160  imainrect  5174  rnsnopg  5207  cnvssrndm  5250  cocnvss  5254  unidmrn  5261  dfdm2  5263  cnvexg  5266  fncnv  5387  funcnvres  5394  funimacnv  5397  fimacnvdisj  5512  dff1o4  5582  foimacnv  5592  funcocnv2  5599  f1ompt  5788  errn  6710  funrnfi  7120  sbthlemi5  7139  sbthlemi8  7142  sbthlemi9  7143  casefun  7263  caseinj  7267  djufun  7282  djuinj  7284  ctssdccl  7289  exmidfodomrlemim  7390  znleval  14632