Definition df-rn 4596

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 4595). For alternate definitions, see dfrn2 4773, dfrn3 4774, and dfrn4 5045. 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 A = dom `' A

Detailed syntax breakdown of Definition df-rn

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	crn 4586	. 2 class ran A
3	1	ccnv 4584	. . 3 class `' A
4	3	cdm 4585	. 2 class dom `' A
5	2, 4	wceq 1335	1 wff ran A = dom `' A

This definition is referenced by:  dfrn2  4773  dmcnvcnv  4809  rncnvcnv  4810  rneq  4812  rnss  4815  brelrng  4816  nfrn  4830  rncoss  4855  rncoeq  4858  cnvimarndm  4949  rnun  4993  rnin  4994  rnxpm  5014  rnxpss  5016  imainrect  5030  rnsnopg  5063  cnvssrndm  5106  cocnvss  5110  unidmrn  5117  dfdm2  5119  cnvexg  5122  fncnv  5235  funcnvres  5242  funimacnv  5245  fimacnvdisj  5353  dff1o4  5421  foimacnv  5431  funcocnv2  5438  f1ompt  5617  errn  6499  funrnfi  6883  sbthlemi5  6902  sbthlemi8  6905  sbthlemi9  6906  casefun  7023  caseinj  7027  djufun  7042  djuinj  7044  ctssdccl  7049  exmidfodomrlemim  7130