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

Definition df-res 4893
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression  ( exp  |`  RR ) (used in reeff1 12726) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 12675 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 21754). (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 4883 . 2  class  ( A  |`  B )
4 cvv 2958 . . . 4  class  _V
52, 4cxp 4879 . . 3  class  ( B  X.  _V )
61, 5cin 3321 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1653 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  reseq1  5143  reseq2  5144  nfres  5151  csbresg  5152  res0  5153  opelres  5154  resres  5162  resundi  5163  resundir  5164  resindi  5165  resindir  5166  inres  5167  resiun1  5168  resiun2  5169  resss  5173  ssres  5175  ssres2  5176  relres  5177  xpssres  5183  resopab  5190  ssrnres  5312  imainrect  5315  xpima  5316  cnvcnv2  5327  resdmres  5364  ressnop0  5916  marypha1lem  7441  dfsup3OLD  7452  gsum2d  15551  gsumxp  15555  pjdm  16939  hausdiag  17682  isngp2  18649  ovoliunlem1  19403  xpdisjres  24041  imadifxp  24043  mbfmcst  24614  0rrv  24714  dfres3  25387  elrn3  25391  dfon4  25743  fndifnfp  26750  csbresgVD  29080
  Copyright terms: Public domain W3C validator