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

Definition df-res 4702
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression  ( exp  |`  RR ) (used in reeff1 12396) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 12345 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 20805). (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 4692 . 2  class  ( A  |`  B )
4 cvv 2791 . . . 4  class  _V
52, 4cxp 4688 . . 3  class  ( B  X.  _V )
61, 5cin 3154 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1625 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  resiundiOLD  4746  reseq1  4950  reseq2  4951  nfres  4958  csbresg  4959  res0  4960  opelres  4961  resres  4969  resundi  4970  resundir  4971  resindi  4972  resindir  4973  inres  4974  resiun1  4975  resiun2  4976  resss  4980  ssres  4982  ssres2  4983  relres  4984  xpssres  4990  resopab  4997  ssrnres  5117  imainrect  5120  cnvcnv2  5128  resdmres  5164  ressnop0  5666  marypha1lem  7183  dfsup3OLD  7194  gsum2d  15219  gsumxp  15223  pjdm  16603  hausdiag  17335  isngp2  18115  ovoliunlem1  18857  dfres3  23521  dfon4  23843  residcp  24477  fndifnfp  26157  csbresgVD  27941
  Copyright terms: Public domain W3C validator