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

Definition df-res 4881
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression  ( exp  |`  RR ) (used in reeff1 12709) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 12658 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 21737). (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 4871 . 2  class  ( A  |`  B )
4 cvv 2948 . . . 4  class  _V
52, 4cxp 4867 . . 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  5131  reseq2  5132  nfres  5139  csbresg  5140  res0  5141  opelres  5142  resres  5150  resundi  5151  resundir  5152  resindi  5153  resindir  5154  inres  5155  resiun1  5156  resiun2  5157  resss  5161  ssres  5163  ssres2  5164  relres  5165  xpssres  5171  resopab  5178  ssrnres  5300  imainrect  5303  xpima  5304  cnvcnv2  5315  resdmres  5352  ressnop0  5904  marypha1lem  7429  dfsup3OLD  7440  gsum2d  15534  gsumxp  15538  pjdm  16922  hausdiag  17665  isngp2  18632  ovoliunlem1  19386  xpdisjres  24024  imadifxp  24026  mbfmcst  24597  0rrv  24697  dfres3  25371  elrn3  25375  dfon4  25688  fndifnfp  26674  csbresgVD  28861
  Copyright terms: Public domain W3C validator