Definition df-rn 4734

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 4733). For alternate definitions, see dfrn2 4916, dfrn3 4917, and dfrn4 5195. 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 4724	. 2 class ran A
3	1	ccnv 4722	. . 3 class `' A
4	3	cdm 4723	. 2 class dom `' A
5	2, 4	wceq 1395	1 wff ran A = dom `' A

This definition is referenced by:  dfrn2  4916  dmcnvcnv  4954  rncnvcnv  4955  rneq  4957  rnss  4960  brelrng  4961  nfrn  4975  rncoss  5001  rncoeq  5004  cnvimarndm  5098  rnun  5143  rnin  5144  rnxpm  5164  rnxpss  5166  imainrect  5180  rnsnopg  5213  cnvssrndm  5256  cocnvss  5260  unidmrn  5267  dfdm2  5269  cnvexg  5272  fncnv  5393  funcnvres  5400  funimacnv  5403  fimacnvdisj  5518  dff1o4  5588  foimacnv  5598  funcocnv2  5605  f1ompt  5794  errn  6719  funrnfi  7135  sbthlemi5  7154  sbthlemi8  7157  sbthlemi9  7158  casefun  7278  caseinj  7282  djufun  7297  djuinj  7299  ctssdccl  7304  exmidfodomrlemim  7405  znleval  14660