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

Definition df-res 4849
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression  ( exp  |`  RR ) (used in reeff1 12676) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 12625 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 21702). (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 4839 . 2  class  ( A  |`  B )
4 cvv 2916 . . . 4  class  _V
52, 4cxp 4835 . . 3  class  ( B  X.  _V )
61, 5cin 3279 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1649 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  reseq1  5099  reseq2  5100  nfres  5107  csbresg  5108  res0  5109  opelres  5110  resres  5118  resundi  5119  resundir  5120  resindi  5121  resindir  5122  inres  5123  resiun1  5124  resiun2  5125  resss  5129  ssres  5131  ssres2  5132  relres  5133  xpssres  5139  resopab  5146  ssrnres  5268  imainrect  5271  xpima  5272  cnvcnv2  5283  resdmres  5320  ressnop0  5872  marypha1lem  7396  dfsup3OLD  7407  gsum2d  15501  gsumxp  15505  pjdm  16889  hausdiag  17630  isngp2  18597  ovoliunlem1  19351  xpdisjres  23989  imadifxp  23991  mbfmcst  24562  0rrv  24662  dfres3  25330  elrn3  25334  dfon4  25647  fndifnfp  26627  csbresgVD  28716
  Copyright terms: Public domain W3C validator