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

Definition df-res 4866
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression  ( exp  |`  RR ) (used in reeff1 14152) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 14099 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 25736). (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 4856 . 2  class  ( A  |`  B )
4 cvv 3087 . . . 4  class  _V
52, 4cxp 4852 . . 3  class  ( B  X.  _V )
61, 5cin 3441 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1437 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff setvar class
This definition is referenced by:  reseq1  5119  reseq2  5120  nfres  5127  csbres  5128  res0  5129  opelres  5130  resres  5137  resundi  5138  resundir  5139  resindi  5140  resindir  5141  inres  5142  resiun1  5143  resiun2  5144  resss  5148  ssres  5150  ssres2  5151  relres  5152  xpssres  5159  resopab  5171  ssrnres  5295  imainrect  5298  xpima  5299  cnvcnv2  5309  resdmres  5346  ressnop0  6086  fndifnfp  6108  tpres  6132  marypha1lem  7953  gsum2d  17539  gsumxp  17543  pjdm  19201  hausdiag  20591  isngp2  21542  ovoliunlem1  22333  xpdisjres  28048  difres  28050  imadifxp  28051  mbfmcst  28920  0rrv  29110  dfres3  30186  elrn3  30190  dfon4  30445  restrreld  35897  xpheOLD  36013  csbresgOLD  36855  csbresgVD  36931
  Copyright terms: Public domain W3C validator