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

Definition df-res 4890
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression  ( exp  |`  RR ) (used in reeff1 12721) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 12670 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 21749). (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 4880 . 2  class  ( A  |`  B )
4 cvv 2956 . . . 4  class  _V
52, 4cxp 4876 . . 3  class  ( B  X.  _V )
61, 5cin 3319 . 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  5140  reseq2  5141  nfres  5148  csbresg  5149  res0  5150  opelres  5151  resres  5159  resundi  5160  resundir  5161  resindi  5162  resindir  5163  inres  5164  resiun1  5165  resiun2  5166  resss  5170  ssres  5172  ssres2  5173  relres  5174  xpssres  5180  resopab  5187  ssrnres  5309  imainrect  5312  xpima  5313  cnvcnv2  5324  resdmres  5361  ressnop0  5913  marypha1lem  7438  dfsup3OLD  7449  gsum2d  15546  gsumxp  15550  pjdm  16934  hausdiag  17677  isngp2  18644  ovoliunlem1  19398  xpdisjres  24036  imadifxp  24038  mbfmcst  24609  0rrv  24709  dfres3  25382  elrn3  25386  dfon4  25738  fndifnfp  26737  csbresgVD  29007
  Copyright terms: Public domain W3C validator