Definition df-rn 4731

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 4730). For alternate definitions, see dfrn2 4913, dfrn3 4914, and dfrn4 5192. 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 4721	. 2 class ran A
3	1	ccnv 4719	. . 3 class `' A
4	3	cdm 4720	. 2 class dom `' A
5	2, 4	wceq 1395	1 wff ran A = dom `' A

This definition is referenced by:  dfrn2  4913  dmcnvcnv  4951  rncnvcnv  4952  rneq  4954  rnss  4957  brelrng  4958  nfrn  4972  rncoss  4998  rncoeq  5001  cnvimarndm  5095  rnun  5140  rnin  5141  rnxpm  5161  rnxpss  5163  imainrect  5177  rnsnopg  5210  cnvssrndm  5253  cocnvss  5257  unidmrn  5264  dfdm2  5266  cnvexg  5269  fncnv  5390  funcnvres  5397  funimacnv  5400  fimacnvdisj  5515  dff1o4  5585  foimacnv  5595  funcocnv2  5602  f1ompt  5791  errn  6715  funrnfi  7125  sbthlemi5  7144  sbthlemi8  7147  sbthlemi9  7148  casefun  7268  caseinj  7272  djufun  7287  djuinj  7289  ctssdccl  7294  exmidfodomrlemim  7395  znleval  14638