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

Definition df-res 4865
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression  ( exp  |`  RR ) (used in reeff1 14173) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 14120 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 25889). (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 4855 . 2  class  ( A  |`  B )
4 cvv 3080 . . . 4  class  _V
52, 4cxp 4851 . . 3  class  ( B  X.  _V )
61, 5cin 3435 . 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  5118  reseq2  5119  nfres  5126  csbres  5127  res0  5128  opelres  5129  resres  5136  resundi  5137  resundir  5138  resindi  5139  resindir  5140  inres  5141  resiun1  5142  resiun2  5143  resss  5147  ssres  5149  ssres2  5150  relres  5151  xpssres  5158  resopab  5170  ssrnres  5294  imainrect  5297  xpima  5298  cnvcnv2  5308  resdmres  5345  ressnop0  6086  fndifnfp  6108  tpres  6132  marypha1lem  7956  gsum2d  17603  gsumxp  17607  pjdm  19268  hausdiag  20658  isngp2  21609  ovoliunlem1  22453  xpdisjres  28211  difres  28213  imadifxp  28214  mbfmcst  29089  0rrv  29292  dfres3  30406  elrn3  30410  dfon4  30665  restrreld  36229  xpheOLD  36347  csbresgOLD  37189  csbresgVD  37265
  Copyright terms: Public domain W3C validator