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

Definition df-res 4701
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression  ( exp  |`  RR ) (used in reeff1 12400) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 12349 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 20828). (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 4691 . 2  class  ( A  |`  B )
4 cvv 2788 . . . 4  class  _V
52, 4cxp 4687 . . 3  class  ( B  X.  _V )
61, 5cin 3151 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1623 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  resiundiOLD  4745  reseq1  4949  reseq2  4950  nfres  4957  csbresg  4958  res0  4959  opelres  4960  resres  4968  resundi  4969  resundir  4970  resindi  4971  resindir  4972  inres  4973  resiun1  4974  resiun2  4975  resss  4979  ssres  4981  ssres2  4982  relres  4983  xpssres  4989  resopab  4996  ssrnres  5116  imainrect  5119  cnvcnv2  5127  resdmres  5164  ressnop0  5703  marypha1lem  7186  dfsup3OLD  7197  gsum2d  15223  gsumxp  15227  pjdm  16607  hausdiag  17339  isngp2  18119  ovoliunlem1  18861  xpdisjres  23197  xpima  23202  mbfmcst  23564  0rrv  23654  dfres3  24116  elrn3  24120  dfon4  24433  residcp  25077  fndifnfp  26756  csbresgVD  28671
  Copyright terms: Public domain W3C validator