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

Definition df-res 5016
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (used in reeff1 13855) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 13803 defines the exponential function, which normally allows the exponent to be a complex number). Another example is that ( ={<.2,6>.,<.3,9>.} /\ ={1,2})->( |` )={<.2,6>.} (ex-res 25162). (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 5006 . 2
4 cvv 3109 . . . 4
52, 4cxp 5002 . . 3
61, 5cin 3474 . 2
73, 6wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  reseq1  5272  reseq2  5273  nfres  5280  csbres  5281  csbresgOLD  5282  res0  5283  opelres  5284  resres  5291  resundi  5292  resundir  5293  resindi  5294  resindir  5295  inres  5296  resiun1  5297  resiun2  5298  resss  5302  ssres  5304  ssres2  5305  relres  5306  xpssres  5313  resopab  5325  ssrnres  5450  imainrect  5453  xpima  5454  cnvcnv2  5465  resdmres  5503  ressnop0  6078  fndifnfp  6100  marypha1lem  7913  dfsup3OLD  7924  gsum2d  16999  gsum2dOLD  17000  gsumxp  17004  gsumxpOLD  17006  pjdm  18738  hausdiag  20146  isngp2  21117  ovoliunlem1  21913  xpdisjres  27455  difres  27457  imadifxp  27458  mbfmcst  28230  0rrv  28390  dfres3  29188  elrn3  29192  dfon4  29543  tpres  32554  csbresgVD  33695  restrreld  37781  xphe  37804
  Copyright terms: Public domain W3C validator