Definition df-rn 4671

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 4670). For alternate definitions, see dfrn2 4851, dfrn3 4852, and dfrn4 5127. 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 4661	. 2 class ran A
3	1	ccnv 4659	. . 3 class `' A
4	3	cdm 4660	. 2 class dom `' A
5	2, 4	wceq 1364	1 wff ran A = dom `' A

This definition is referenced by:  dfrn2  4851  dmcnvcnv  4887  rncnvcnv  4888  rneq  4890  rnss  4893  brelrng  4894  nfrn  4908  rncoss  4933  rncoeq  4936  cnvimarndm  5030  rnun  5075  rnin  5076  rnxpm  5096  rnxpss  5098  imainrect  5112  rnsnopg  5145  cnvssrndm  5188  cocnvss  5192  unidmrn  5199  dfdm2  5201  cnvexg  5204  fncnv  5321  funcnvres  5328  funimacnv  5331  fimacnvdisj  5439  dff1o4  5509  foimacnv  5519  funcocnv2  5526  f1ompt  5710  errn  6611  funrnfi  7003  sbthlemi5  7022  sbthlemi8  7025  sbthlemi9  7026  casefun  7146  caseinj  7150  djufun  7165  djuinj  7167  ctssdccl  7172  exmidfodomrlemim  7263  znleval  14152