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

Definition df-res 5001
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression  ( exp  |`  RR ) (used in reeff1 13837) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 13785 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 25140). (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 4991 . 2  class  ( A  |`  B )
4 cvv 3095 . . . 4  class  _V
52, 4cxp 4987 . . 3  class  ( B  X.  _V )
61, 5cin 3460 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1383 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff setvar class
This definition is referenced by:  reseq1  5257  reseq2  5258  nfres  5265  csbres  5266  csbresgOLD  5267  res0  5268  opelres  5269  resres  5276  resundi  5277  resundir  5278  resindi  5279  resindir  5280  inres  5281  resiun1  5282  resiun2  5283  resss  5287  ssres  5289  ssres2  5290  relres  5291  xpssres  5298  resopab  5310  ssrnres  5435  imainrect  5438  xpima  5439  cnvcnv2  5450  resdmres  5488  ressnop0  6063  fndifnfp  6085  marypha1lem  7895  dfsup3OLD  7906  gsum2d  16978  gsum2dOLD  16979  gsumxp  16983  gsumxpOLD  16985  pjdm  18716  hausdiag  20124  isngp2  21095  ovoliunlem1  21891  xpdisjres  27433  difres  27435  imadifxp  27436  mbfmcst  28208  0rrv  28368  dfres3  29164  elrn3  29168  dfon4  29519  tpres  32506  csbresgVD  33563  restrreld  37609  xphe  37626
  Copyright terms: Public domain W3C validator