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

Definition df-res 5006
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression  ( exp  |`  RR ) (used in reeff1 13707) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 13656 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 24827). (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 4996 . 2  class  ( A  |`  B )
4 cvv 3108 . . . 4  class  _V
52, 4cxp 4992 . . 3  class  ( B  X.  _V )
61, 5cin 3470 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1374 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff setvar class
This definition is referenced by:  reseq1  5260  reseq2  5261  nfres  5268  csbres  5269  csbresgOLD  5270  res0  5271  opelres  5272  resres  5279  resundi  5280  resundir  5281  resindi  5282  resindir  5283  inres  5284  resiun1  5285  resiun2  5286  resss  5290  ssres  5292  ssres2  5293  relres  5294  xpssres  5301  resopab  5313  ssrnres  5438  imainrect  5441  xpima  5442  cnvcnv2  5453  resdmres  5491  ressnop0  6061  fndifnfp  6083  marypha1lem  7884  dfsup3OLD  7895  gsum2d  16785  gsum2dOLD  16786  gsumxp  16790  gsumxpOLD  16792  pjdm  18500  hausdiag  19876  isngp2  20847  ovoliunlem1  21643  xpdisjres  27116  difres  27118  imadifxp  27119  mbfmcst  27858  0rrv  28018  dfres3  28753  elrn3  28757  dfon4  29108  csbresgVD  32652  restrreld  36668
  Copyright terms: Public domain W3C validator