Definition df-rn 4783

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 4782). For alternate definitions, see dfrn2 4966, dfrn3 4967, and dfrn4 5246. 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 4773	. 2 class ran A
3	1	ccnv 4771	. . 3 class `' A
4	3	cdm 4772	. 2 class dom `' A
5	2, 4	wceq 1402	1 wff ran A = dom `' A

This definition is referenced by:  dfrn2  4966  dmcnvcnv  5004  rncnvcnv  5005  rneq  5007  rnss  5010  brelrng  5011  nfrn  5025  rncoss  5051  rncoeq  5054  cnvimarndm  5149  rnun  5194  rnin  5195  rnxpm  5215  rnxpss  5217  imainrect  5231  rnsnopg  5264  cnvssrndm  5307  cocnvss  5311  unidmrn  5318  dfdm2  5320  cnvexg  5323  fncnv  5445  funcnvres  5452  funimacnv  5455  fimacnvdisj  5574  dff1o4  5645  foimacnv  5655  funcocnv2  5662  f1ompt  5853  errn  6823  funrnfi  7250  sbthlemi5  7272  sbthlemi8  7275  sbthlemi9  7276  casefun  7419  caseinj  7423  djufun  7438  djuinj  7440  ctssdccl  7445  exmidfodomrlemim  7547  znleval  14971