Definition df-rn 4730

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 4729). For alternate definitions, see dfrn2 4910, dfrn3 4911, and dfrn4 5189. 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 4720	. 2 class ran A
3	1	ccnv 4718	. . 3 class `' A
4	3	cdm 4719	. 2 class dom `' A
5	2, 4	wceq 1395	1 wff ran A = dom `' A

This definition is referenced by:  dfrn2  4910  dmcnvcnv  4948  rncnvcnv  4949  rneq  4951  rnss  4954  brelrng  4955  nfrn  4969  rncoss  4995  rncoeq  4998  cnvimarndm  5092  rnun  5137  rnin  5138  rnxpm  5158  rnxpss  5160  imainrect  5174  rnsnopg  5207  cnvssrndm  5250  cocnvss  5254  unidmrn  5261  dfdm2  5263  cnvexg  5266  fncnv  5387  funcnvres  5394  funimacnv  5397  fimacnvdisj  5510  dff1o4  5580  foimacnv  5590  funcocnv2  5597  f1ompt  5786  errn  6702  funrnfi  7109  sbthlemi5  7128  sbthlemi8  7131  sbthlemi9  7132  casefun  7252  caseinj  7256  djufun  7271  djuinj  7273  ctssdccl  7278  exmidfodomrlemim  7379  znleval  14617