Definition df-rn 4704

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 4703). For alternate definitions, see dfrn2 4884, dfrn3 4885, and dfrn4 5162. 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 4694	. 2 class ran A
3	1	ccnv 4692	. . 3 class `' A
4	3	cdm 4693	. 2 class dom `' A
5	2, 4	wceq 1373	1 wff ran A = dom `' A

This definition is referenced by:  dfrn2  4884  dmcnvcnv  4921  rncnvcnv  4922  rneq  4924  rnss  4927  brelrng  4928  nfrn  4942  rncoss  4968  rncoeq  4971  cnvimarndm  5065  rnun  5110  rnin  5111  rnxpm  5131  rnxpss  5133  imainrect  5147  rnsnopg  5180  cnvssrndm  5223  cocnvss  5227  unidmrn  5234  dfdm2  5236  cnvexg  5239  fncnv  5359  funcnvres  5366  funimacnv  5369  fimacnvdisj  5482  dff1o4  5552  foimacnv  5562  funcocnv2  5569  f1ompt  5754  errn  6665  funrnfi  7070  sbthlemi5  7089  sbthlemi8  7092  sbthlemi9  7093  casefun  7213  caseinj  7217  djufun  7232  djuinj  7234  ctssdccl  7239  exmidfodomrlemim  7340  znleval  14530