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 5323
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 15066) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 15014 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 27625). (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 5313 . 2 class (𝐴𝐵)
4 cvv 3391 . . . 4 class V
52, 4cxp 5309 . . 3 class (𝐵 × V)
61, 5cin 3768 . 2 class (𝐴 ∩ (𝐵 × V))
73, 6wceq 1637 1 wff (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
Colors of variables: wff setvar class
This definition is referenced by:  reseq1  5591  reseq2  5592  nfres  5599  csbres  5600  res0  5601  dfres3  5602  opelresg  5603  opelresOLD  5607  resres  5613  resundi  5614  resundir  5615  resindi  5616  resindir  5617  inres  5618  resdifcom  5619  resiun1  5620  resiun2  5621  resss  5625  ssres  5627  ssres2  5628  relres  5629  xpssres  5636  elres  5638  resopab  5651  elrid  5662  ssrnres  5783  imainrect  5786  xpima  5787  cnvcnv2  5799  resdmres  5839  ressnop0  6640  fndifnfp  6663  tpres  6687  marypha1lem  8574  gsum2d  18568  gsumxp  18572  pjdm  20257  hausdiag  21658  isngp2  22610  ovoliunlem1  23479  xpdisjres  29732  difres  29734  imadifxp  29735  mbfmcst  30642  0rrv  30834  elrn3  31969  nosupbnd2lem1  32177  noetalem2  32180  noetalem3  32181  dfon4  32316  opelresALTV  34344  inxpssres  34387  restrreld  38453  csbresgOLD  39544  csbresgVD  39619
  Copyright terms: Public domain W3C validator