Definition df-rn 4759

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 4758). For alternate definitions, see dfrn2 4942, dfrn3 4943, and dfrn4 5222. 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 4749	. 2 class ran A
3	1	ccnv 4747	. . 3 class `' A
4	3	cdm 4748	. 2 class dom `' A
5	2, 4	wceq 1398	1 wff ran A = dom `' A

This definition is referenced by:  dfrn2  4942  dmcnvcnv  4980  rncnvcnv  4981  rneq  4983  rnss  4986  brelrng  4987  nfrn  5001  rncoss  5027  rncoeq  5030  cnvimarndm  5125  rnun  5170  rnin  5171  rnxpm  5191  rnxpss  5193  imainrect  5207  rnsnopg  5240  cnvssrndm  5283  cocnvss  5287  unidmrn  5294  dfdm2  5296  cnvexg  5299  fncnv  5421  funcnvres  5428  funimacnv  5431  fimacnvdisj  5550  dff1o4  5621  foimacnv  5631  funcocnv2  5638  f1ompt  5827  errn  6788  funrnfi  7208  sbthlemi5  7230  sbthlemi8  7233  sbthlemi9  7234  casefun  7375  caseinj  7379  djufun  7394  djuinj  7396  ctssdccl  7401  exmidfodomrlemim  7503  znleval  14788