Definition df-rn 4687

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 4686). For alternate definitions, see dfrn2 4867, dfrn3 4868, and dfrn4 5144. 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 4677	. 2 class ran A
3	1	ccnv 4675	. . 3 class `' A
4	3	cdm 4676	. 2 class dom `' A
5	2, 4	wceq 1373	1 wff ran A = dom `' A

This definition is referenced by:  dfrn2  4867  dmcnvcnv  4903  rncnvcnv  4904  rneq  4906  rnss  4909  brelrng  4910  nfrn  4924  rncoss  4950  rncoeq  4953  cnvimarndm  5047  rnun  5092  rnin  5093  rnxpm  5113  rnxpss  5115  imainrect  5129  rnsnopg  5162  cnvssrndm  5205  cocnvss  5209  unidmrn  5216  dfdm2  5218  cnvexg  5221  fncnv  5341  funcnvres  5348  funimacnv  5351  fimacnvdisj  5462  dff1o4  5532  foimacnv  5542  funcocnv2  5549  f1ompt  5733  errn  6644  funrnfi  7046  sbthlemi5  7065  sbthlemi8  7068  sbthlemi9  7069  casefun  7189  caseinj  7193  djufun  7208  djuinj  7210  ctssdccl  7215  exmidfodomrlemim  7311  znleval  14448