Definition df-rn 4614

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 4613). For alternate definitions, see dfrn2 4791, dfrn3 4792, and dfrn4 5063. 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 4604	. 2 class ran A
3	1	ccnv 4602	. . 3 class `' A
4	3	cdm 4603	. 2 class dom `' A
5	2, 4	wceq 1343	1 wff ran A = dom `' A

This definition is referenced by:  dfrn2  4791  dmcnvcnv  4827  rncnvcnv  4828  rneq  4830  rnss  4833  brelrng  4834  nfrn  4848  rncoss  4873  rncoeq  4876  cnvimarndm  4967  rnun  5011  rnin  5012  rnxpm  5032  rnxpss  5034  imainrect  5048  rnsnopg  5081  cnvssrndm  5124  cocnvss  5128  unidmrn  5135  dfdm2  5137  cnvexg  5140  fncnv  5253  funcnvres  5260  funimacnv  5263  fimacnvdisj  5371  dff1o4  5439  foimacnv  5449  funcocnv2  5456  f1ompt  5635  errn  6519  funrnfi  6903  sbthlemi5  6922  sbthlemi8  6925  sbthlemi9  6926  casefun  7046  caseinj  7050  djufun  7065  djuinj  7067  ctssdccl  7072  exmidfodomrlemim  7153