MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rn Unicode version

Definition df-rn 4700
Description: Define the range of a class. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ran  F  =  { 6 ,  9 } (ex-rn 20803). Contrast with domain (defined in df-dm 4699). For alternate definitions, see dfrn2 4868, dfrn3 4869, and dfrn4 5133. 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
StepHypRef Expression
1 cA . . 3  class  A
21crn 4690 . 2  class  ran  A
31ccnv 4688 . . 3  class  `' A
43cdm 4689 . 2  class  dom  `'  A
52, 4wceq 1624 1  wff  ran  A  =  dom  `'  A
Colors of variables: wff set class
This definition is referenced by:  dfrn2  4868  dmcnvcnv  4901  rncnvcnv  4902  rneq  4904  rnss  4907  brelrng  4908  nfrn  4921  rncoss  4945  rncoeq  4948  cnvimarndm  5034  rnun  5089  rnin  5090  rnxp  5106  rnxpss  5108  imainrect  5119  rnsnopg  5151  cnvssrndm  5193  unidmrn  5201  dfdm2  5203  cnvexg  5207  fncnv  5280  funcnvres  5287  funimacnv  5290  fimacnvdisj  5385  dff1o4  5446  foimacnv  5456  funcocnv2  5464  f1ompt  5644  tz7.48-3  6452  errn  6678  omxpenlem  6959  sbthlem5  6971  sbthlem8  6974  sbthlem9  6975  fodomr  7008  domss2  7016  rnfi  7137  zorn2lem4  8122  fpwwe2lem13  8260  invf  13665  cnvtsr  14326  znleval  16503  ordtbas2  16916  ordtcnv  16926  ordtrest2  16929  cnconn  17143  tgqtop  17398  adj1o  22467  nvof1o  23030  fldcnv  24455  rnintintrn  24526  domcnvpre  24633  ranncnt  24683  toplat  24690
  Copyright terms: Public domain W3C validator