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

Definition df-res 4823
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (used in reeff1 13344) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 13293 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 23327). (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 4813 . 2
4 cvv 2951 . . . 4
52, 4cxp 4809 . . 3
61, 5cin 3304 . 2
73, 6wceq 1687 1
Colors of variables: wff setvar class
This definition is referenced by:  reseq1  5075  reseq2  5076  nfres  5083  csbres  5084  csbresgOLD  5085  res0  5086  opelres  5087  resres  5095  resundi  5096  resundir  5097  resindi  5098  resindir  5099  inres  5100  resiun1  5101  resiun2  5102  resss  5106  ssres  5108  ssres2  5109  relres  5110  xpssres  5116  resopab  5125  ssrnres  5248  imainrect  5251  xpima  5252  cnvcnv2  5263  resdmres  5301  ressnop0  5858  fndifnfp  5876  marypha1lem  7630  dfsup3OLD  7641  gsum2d  16355  gsumxp  16359  pjdm  17840  hausdiag  18922  isngp2  19889  ovoliunlem1  20685  xpdisjres  25618  imadifxp  25619  mbfmcst  26383  0rrv  26537  dfres3  27271  elrn3  27275  dfon4  27626  gsumX2d  30504  gsumXxp  30508  csbresgVD  31209
  Copyright terms: Public domain W3C validator