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

Definition df-res 4667
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression  ( exp  |`  RR ) (used in reeff1 12348) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 12297 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 20757). (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 4649 . 2  class  ( A  |`  B )
4 cvv 2757 . . . 4  class  _V
52, 4cxp 4645 . . 3  class  ( B  X.  _V )
61, 5cin 3112 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1619 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  resiundiOLD  4719  reseq1  4923  reseq2  4924  nfres  4931  csbresg  4932  res0  4933  opelres  4934  resres  4942  resundi  4943  resundir  4944  resindi  4945  resindir  4946  inres  4947  resiun1  4948  resiun2  4949  resss  4953  ssres  4955  ssres2  4956  relres  4957  xpssres  4963  resopab  4970  ssrnres  5090  imainrect  5093  cnvcnv2  5101  resdmres  5137  ressnop0  5623  marypha1lem  7140  dfsup3OLD  7151  gsum2d  15171  gsumxp  15175  pjdm  16555  hausdiag  17287  isngp2  18067  ovoliunlem1  18809  dfres3  23473  dfon4  23795  residcp  24429  fndifnfp  26109  csbresgVD  27705
  Copyright terms: Public domain W3C validator