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

Definition df-res 4868
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression  ( exp  |`  RR ) (used in reeff1 14229) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 14176 defines the exponential function, which normally allows the exponent to be a complex number). Another example is that  ( F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  /\  B  =  { 1 ,  2 } )  ->  ( F  |`  B )  =  { <. 2 ,  6
>. } (ex-res 25947). (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
df-res  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )

Detailed syntax breakdown of Definition df-res
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2cres 4858 . 2  class  ( A  |`  B )
4 cvv 3057 . . . 4  class  _V
52, 4cxp 4854 . . 3  class  ( B  X.  _V )
61, 5cin 3415 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1455 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff setvar class
This definition is referenced by:  reseq1  5121  reseq2  5122  nfres  5129  csbres  5130  res0  5131  opelres  5132  resres  5139  resundi  5140  resundir  5141  resindi  5142  resindir  5143  inres  5144  resiun1  5145  resiun2  5146  resss  5150  ssres  5152  ssres2  5153  relres  5154  xpssres  5161  resopab  5173  ssrnres  5297  imainrect  5300  xpima  5301  cnvcnv2  5312  resdmres  5349  ressnop0  6100  fndifnfp  6122  tpres  6146  marypha1lem  7978  gsum2d  17659  gsumxp  17663  pjdm  19325  hausdiag  20715  isngp2  21666  ovoliunlem1  22510  xpdisjres  28262  difres  28264  imadifxp  28265  mbfmcst  29131  0rrv  29334  dfres3  30449  elrn3  30453  dfon4  30710  restrreld  36305  xpheOLD  36423  csbresgOLD  37257  csbresgVD  37333
  Copyright terms: Public domain W3C validator