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

Definition df-res 4874
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (used in reeff1 13251) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 13200 defines the exponential function, which normally allows the exponent to be a complex number). Another example is that ( ={<.2,6>.,<.3,9>.} /\B={1,2})->( |`B)={<.2,6>.} (ex-res 22770). (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
df-res

Detailed syntax breakdown of Definition df-res
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2cres 4864 . 2
4 cvv 3015 . . . 4
52, 4cxp 4860 . . 3
61, 5cin 3364 . 2
73, 6wceq 1670 1
Colors of variables: wff set class
This definition is referenced by:  reseq1  5126  reseq2  5127  nfres  5134  csbres  5135  csbresgOLD  5136  res0  5137  opelres  5138  resres  5146  resundi  5147  resundir  5148  resindi  5149  resindir  5150  inres  5151  resiun1  5152  resiun2  5153  resss  5157  ssres  5159  ssres2  5160  relres  5161  xpssres  5167  resopab  5176  ssrnres  5297  imainrect  5300  xpima  5301  cnvcnv2  5311  resdmres  5349  ressnop0  5904  fndifnfp  5922  marypha1lem  7605  dfsup3OLD  7616  gsum2d  16161  gsumxp  16165  pjdm  17559  hausdiag  18692  isngp2  19659  ovoliunlem1  20413  xpdisjres  25066  imadifxp  25067  mbfmcst  25854  0rrv  25984  dfres3  26721  elrn3  26725  dfon4  27077  csbresgVD  30477
  Copyright terms: Public domain W3C validator