Definition df-rn 4299

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 4298). For alternate definitions, see dfrn2 4466, dfrn3 4467, and dfrn4 4724. 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 4289	. 2 class ran A
3	1	ccnv 4287	. . 3 class `'A
4	3	cdm 4288	. 2 class dom `'A
5	2, 4	wceq 1242	1 wff ran A = dom `'A

This definition is referenced by:  dfrn2  4466  dmcnvcnv  4501  rncnvcnv  4502  rneq  4504  rnss  4507  brelrng  4508  nfrn  4522  rncoss  4545  rncoeq  4548  cnvimarndm  4632  rnun  4675  rnin  4676  rnxpm  4695  rnxpss  4697  imainrect  4709  rnsnopg  4742  cnvssrndm  4785  unidmrn  4793  dfdm2  4795  cnvexg  4798  fncnv  4908  funcnvres  4915  funimacnv  4918  fimacnvdisj  5017  dff1o4  5077  foimacnv  5087  funcocnv2  5094  f1ompt  5263  errn  6064