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 5155
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 14894) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 14842 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 27428). (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 5145 . 2 class (𝐴𝐵)
4 cvv 3231 . . . 4 class V
52, 4cxp 5141 . . 3 class (𝐵 × V)
61, 5cin 3606 . 2 class (𝐴 ∩ (𝐵 × V))
73, 6wceq 1523 1 wff (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
Colors of variables: wff setvar class
This definition is referenced by:  reseq1  5422  reseq2  5423  nfres  5430  csbres  5431  res0  5432  dfres3  5433  opelresg  5434  opelresOLD  5438  resres  5444  resundi  5445  resundir  5446  resindi  5447  resindir  5448  inres  5449  resdifcom  5450  resiun1  5451  resiun1OLD  5452  resiun2  5453  resss  5457  ssres  5459  ssres2  5460  relres  5461  xpssres  5469  resopab  5481  ssrnres  5607  imainrect  5610  xpima  5611  cnvcnv2  5623  resdmres  5663  ressnop0  6460  fndifnfp  6483  tpres  6507  marypha1lem  8380  gsum2d  18417  gsumxp  18421  pjdm  20099  hausdiag  21496  isngp2  22448  ovoliunlem1  23316  xpdisjres  29537  difres  29539  imadifxp  29540  mbfmcst  30449  0rrv  30641  elrn3  31778  nosupbnd2lem1  31986  noetalem2  31989  noetalem3  31990  dfon4  32125  opelresALTV  34172  inxpssres  34217  restrreld  38276  csbresgOLD  39370  csbresgVD  39445
  Copyright terms: Public domain W3C validator