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

Definition df-res 4717
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression  ( exp  |`  RR ) (used in reeff1 12416) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 12365 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 20844). (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 4707 . 2  class  ( A  |`  B )
4 cvv 2801 . . . 4  class  _V
52, 4cxp 4703 . . 3  class  ( B  X.  _V )
61, 5cin 3164 . 2  class  ( A  i^i  ( B  X.  _V ) )
73, 6wceq 1632 1  wff  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  resiundiOLD  4761  reseq1  4965  reseq2  4966  nfres  4973  csbresg  4974  res0  4975  opelres  4976  resres  4984  resundi  4985  resundir  4986  resindi  4987  resindir  4988  inres  4989  resiun1  4990  resiun2  4991  resss  4995  ssres  4997  ssres2  4998  relres  4999  xpssres  5005  resopab  5012  ssrnres  5132  imainrect  5135  cnvcnv2  5143  resdmres  5180  ressnop0  5719  marypha1lem  7202  dfsup3OLD  7213  gsum2d  15239  gsumxp  15243  pjdm  16623  hausdiag  17355  isngp2  18135  ovoliunlem1  18877  xpdisjres  23212  xpima  23217  mbfmcst  23579  0rrv  23669  dfres3  24187  elrn3  24191  dfon4  24504  residcp  25180  fndifnfp  26859  csbresgVD  28987
  Copyright terms: Public domain W3C validator