Definition df-rn 4356

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 4355). For alternate definitions, see dfrn2 4523, dfrn3 4524, and dfrn4 4781. 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 4346	. 2 class ran A
3	1	ccnv 4344	. . 3 class `' A
4	3	cdm 4345	. 2 class dom `' A
5	2, 4	wceq 1243	1 wff ran A = dom `' A

This definition is referenced by:  dfrn2  4523  dmcnvcnv  4558  rncnvcnv  4559  rneq  4561  rnss  4564  brelrng  4565  nfrn  4579  rncoss  4602  rncoeq  4605  cnvimarndm  4689  rnun  4732  rnin  4733  rnxpm  4752  rnxpss  4754  imainrect  4766  rnsnopg  4799  cnvssrndm  4842  unidmrn  4850  dfdm2  4852  cnvexg  4855  fncnv  4965  funcnvres  4972  funimacnv  4975  fimacnvdisj  5074  dff1o4  5134  foimacnv  5144  funcocnv2  5151  f1ompt  5320  errn  6128