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

Definition df-res 4893
 Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (used in reeff1 12726) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 12675 defines the exponential function, which normally allows the exponent to be a complex number). Another example is that (ex-res 21754). (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 4883 . 2
4 cvv 2958 . . . 4
52, 4cxp 4879 . . 3
61, 5cin 3321 . 2
73, 6wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  reseq1  5143  reseq2  5144  nfres  5151  csbresg  5152  res0  5153  opelres  5154  resres  5162  resundi  5163  resundir  5164  resindi  5165  resindir  5166  inres  5167  resiun1  5168  resiun2  5169  resss  5173  ssres  5175  ssres2  5176  relres  5177  xpssres  5183  resopab  5190  ssrnres  5312  imainrect  5315  xpima  5316  cnvcnv2  5327  resdmres  5364  ressnop0  5916  marypha1lem  7441  dfsup3OLD  7452  gsum2d  15551  gsumxp  15555  pjdm  16939  hausdiag  17682  isngp2  18649  ovoliunlem1  19403  xpdisjres  24041  imadifxp  24043  mbfmcst  24614  0rrv  24714  dfres3  25387  elrn3  25391  dfon4  25743  fndifnfp  26750  csbresgVD  29080
 Copyright terms: Public domain W3C validator