Definition df-rn 4736

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 4735). For alternate definitions, see dfrn2 4918, dfrn3 4919, and dfrn4 5197. 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 4726	. 2 class ran A
3	1	ccnv 4724	. . 3 class `' A
4	3	cdm 4725	. 2 class dom `' A
5	2, 4	wceq 1397	1 wff ran A = dom `' A

This definition is referenced by:  dfrn2  4918  dmcnvcnv  4956  rncnvcnv  4957  rneq  4959  rnss  4962  brelrng  4963  nfrn  4977  rncoss  5003  rncoeq  5006  cnvimarndm  5100  rnun  5145  rnin  5146  rnxpm  5166  rnxpss  5168  imainrect  5182  rnsnopg  5215  cnvssrndm  5258  cocnvss  5262  unidmrn  5269  dfdm2  5271  cnvexg  5274  fncnv  5396  funcnvres  5403  funimacnv  5406  fimacnvdisj  5521  dff1o4  5592  foimacnv  5602  funcocnv2  5609  f1ompt  5799  errn  6727  funrnfi  7144  sbthlemi5  7163  sbthlemi8  7166  sbthlemi9  7167  casefun  7287  caseinj  7291  djufun  7306  djuinj  7308  ctssdccl  7313  exmidfodomrlemim  7415  znleval  14689