Definition df-rn 4631

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 4630). For alternate definitions, see dfrn2 4808, dfrn3 4809, and dfrn4 5081. 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 4621	. 2 class ran 𝐴
3	1	ccnv 4619	. . 3 class ◡𝐴
4	3	cdm 4620	. 2 class dom ◡𝐴
5	2, 4	wceq 1353	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4808  dmcnvcnv  4844  rncnvcnv  4845  rneq  4847  rnss  4850  brelrng  4851  nfrn  4865  rncoss  4890  rncoeq  4893  cnvimarndm  4985  rnun  5029  rnin  5030  rnxpm  5050  rnxpss  5052  imainrect  5066  rnsnopg  5099  cnvssrndm  5142  cocnvss  5146  unidmrn  5153  dfdm2  5155  cnvexg  5158  fncnv  5274  funcnvres  5281  funimacnv  5284  fimacnvdisj  5392  dff1o4  5461  foimacnv  5471  funcocnv2  5478  f1ompt  5659  errn  6547  funrnfi  6931  sbthlemi5  6950  sbthlemi8  6953  sbthlemi9  6954  casefun  7074  caseinj  7078  djufun  7093  djuinj  7095  ctssdccl  7100  exmidfodomrlemim  7190