Definition df-rn 4686

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 4685). For alternate definitions, see dfrn2 4866, dfrn3 4867, and dfrn4 5143. 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 4676	. 2 class ran A
3	1	ccnv 4674	. . 3 class `' A
4	3	cdm 4675	. 2 class dom `' A
5	2, 4	wceq 1373	1 wff ran A = dom `' A

This definition is referenced by:  dfrn2  4866  dmcnvcnv  4902  rncnvcnv  4903  rneq  4905  rnss  4908  brelrng  4909  nfrn  4923  rncoss  4949  rncoeq  4952  cnvimarndm  5046  rnun  5091  rnin  5092  rnxpm  5112  rnxpss  5114  imainrect  5128  rnsnopg  5161  cnvssrndm  5204  cocnvss  5208  unidmrn  5215  dfdm2  5217  cnvexg  5220  fncnv  5340  funcnvres  5347  funimacnv  5350  fimacnvdisj  5460  dff1o4  5530  foimacnv  5540  funcocnv2  5547  f1ompt  5731  errn  6642  funrnfi  7044  sbthlemi5  7063  sbthlemi8  7066  sbthlemi9  7067  casefun  7187  caseinj  7191  djufun  7206  djuinj  7208  ctssdccl  7213  exmidfodomrlemim  7309  znleval  14415