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

Definition df-res 4925
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression  ( exp  |`  RR ) (used in reeff1 13857) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 13805 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 25283). (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 4915 . 2  class  ( A  |`  B )
4 cvv 3034 . . . 4  class  _V
52, 4cxp 4911 . . 3  class  ( B  X.  _V )
61, 5cin 3388 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1399 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff setvar class
This definition is referenced by:  reseq1  5180  reseq2  5181  nfres  5188  csbres  5189  res0  5190  opelres  5191  resres  5198  resundi  5199  resundir  5200  resindi  5201  resindir  5202  inres  5203  resiun1  5204  resiun2  5205  resss  5209  ssres  5211  ssres2  5212  relres  5213  xpssres  5220  resopab  5232  ssrnres  5355  imainrect  5358  xpima  5359  cnvcnv2  5369  resdmres  5406  ressnop0  5980  fndifnfp  6002  tpres  6026  marypha1lem  7808  gsum2d  17113  gsum2dOLD  17114  gsumxp  17118  pjdm  18829  hausdiag  20231  isngp2  21202  ovoliunlem1  21998  xpdisjres  27588  difres  27590  imadifxp  27591  mbfmcst  28386  0rrv  28573  dfres3  29354  elrn3  29358  dfon4  29696  csbresgOLD  33966  csbresgVD  34042  restrreld  38206  xpheOLD  38276
  Copyright terms: Public domain W3C validator