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

Definition df-res 5096
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 14794) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 14742 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 27186). (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
df-res (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))

Detailed syntax breakdown of Definition df-res
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cres 5086 . 2 class (𝐴𝐵)
4 cvv 3190 . . . 4 class V
52, 4cxp 5082 . . 3 class (𝐵 × V)
61, 5cin 3559 . 2 class (𝐴 ∩ (𝐵 × V))
73, 6wceq 1480 1 wff (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
Colors of variables: wff setvar class
This definition is referenced by:  reseq1  5360  reseq2  5361  nfres  5368  csbres  5369  res0  5370  opelres  5371  resres  5378  resundi  5379  resundir  5380  resindi  5381  resindir  5382  inres  5383  resdifcom  5384  resiun1  5385  resiun1OLD  5386  resiun2  5387  resss  5391  ssres  5393  ssres2  5394  relres  5395  xpssres  5403  resopab  5415  ssrnres  5541  imainrect  5544  xpima  5545  cnvcnv2  5557  resdmres  5594  ressnop0  6385  fndifnfp  6407  tpres  6431  marypha1lem  8299  gsum2d  18311  gsumxp  18315  pjdm  19991  hausdiag  21388  isngp2  22341  ovoliunlem1  23210  xpdisjres  29297  difres  29299  imadifxp  29300  mbfmcst  30144  0rrv  30336  dfres3  31410  elrn3  31414  dfon4  31695  restrreld  37479  csbresgOLD  38577  csbresgVD  38653
  Copyright terms: Public domain W3C validator