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

Definition df-res 4882
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression  ( exp  |`  RR ) (used in reeff1 12713) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 12662 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 21741). (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 4872 . 2  class  ( A  |`  B )
4 cvv 2948 . . . 4  class  _V
52, 4cxp 4868 . . 3  class  ( B  X.  _V )
61, 5cin 3311 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1652 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  reseq1  5132  reseq2  5133  nfres  5140  csbresg  5141  res0  5142  opelres  5143  resres  5151  resundi  5152  resundir  5153  resindi  5154  resindir  5155  inres  5156  resiun1  5157  resiun2  5158  resss  5162  ssres  5164  ssres2  5165  relres  5166  xpssres  5172  resopab  5179  ssrnres  5301  imainrect  5304  xpima  5305  cnvcnv2  5316  resdmres  5353  ressnop0  5905  marypha1lem  7430  dfsup3OLD  7441  gsum2d  15538  gsumxp  15542  pjdm  16926  hausdiag  17669  isngp2  18636  ovoliunlem1  19390  xpdisjres  24028  imadifxp  24030  mbfmcst  24601  0rrv  24701  dfres3  25374  elrn3  25378  dfon4  25730  fndifnfp  26718  csbresgVD  28934
  Copyright terms: Public domain W3C validator