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  5591  foimacnv  5601  funcocnv2  5608  f1ompt  5798  errn  6724  funrnfi  7141  sbthlemi5  7160  sbthlemi8  7163  sbthlemi9  7164  casefun  7284  caseinj  7288  djufun  7303  djuinj  7305  ctssdccl  7310  exmidfodomrlemim  7412  znleval  14670