Definition df-rn 4558

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 4557). For alternate definitions, see dfrn2 4735, dfrn3 4736, and dfrn4 5007. 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 4548	. 2 class ran A
3	1	ccnv 4546	. . 3 class `' A
4	3	cdm 4547	. 2 class dom `' A
5	2, 4	wceq 1332	1 wff ran A = dom `' A

This definition is referenced by:  dfrn2  4735  dmcnvcnv  4771  rncnvcnv  4772  rneq  4774  rnss  4777  brelrng  4778  nfrn  4792  rncoss  4817  rncoeq  4820  cnvimarndm  4911  rnun  4955  rnin  4956  rnxpm  4976  rnxpss  4978  imainrect  4992  rnsnopg  5025  cnvssrndm  5068  cocnvss  5072  unidmrn  5079  dfdm2  5081  cnvexg  5084  fncnv  5197  funcnvres  5204  funimacnv  5207  fimacnvdisj  5315  dff1o4  5383  foimacnv  5393  funcocnv2  5400  f1ompt  5579  errn  6459  funrnfi  6838  sbthlemi5  6857  sbthlemi8  6860  sbthlemi9  6861  casefun  6978  caseinj  6982  djufun  6997  djuinj  6999  ctssdccl  7004  exmidfodomrlemim  7074