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

Definition df-res 4600
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression  ( exp  |`  RR ) (used in reeff1 12274) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 12223 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 20641). (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 4582 . 2  class  ( A  |`  B )
4 cvv 2727 . . . 4  class  _V
52, 4cxp 4578 . . 3  class  ( B  X.  _V )
61, 5cin 3077 . 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  4652  reseq1  4856  reseq2  4857  nfres  4864  csbresg  4865  res0  4866  opelres  4867  resres  4875  resundi  4876  resundir  4877  resindi  4878  resindir  4879  inres  4880  resiun1  4881  resiun2  4882  resss  4886  ssres  4888  ssres2  4889  relres  4890  xpssres  4896  resopab  4903  ssrnres  5023  imainrect  5026  cnvcnv2  5034  resdmres  5070  ressnop0  5555  marypha1lem  7070  dfsup3OLD  7081  gsum2d  15058  gsumxp  15062  pjdm  16439  hausdiag  17171  isngp2  17951  ovoliunlem1  18693  dfres3  23286  dfon4  23608  residcp  24242  fndifnfp  25922  csbresgVD  27361
  Copyright terms: Public domain W3C validator