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 5039
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 14637) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 14585 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 26483). (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 5029 . 2 class (𝐴𝐵)
4 cvv 3172 . . . 4 class V
52, 4cxp 5025 . . 3 class (𝐵 × V)
61, 5cin 3538 . 2 class (𝐴 ∩ (𝐵 × V))
73, 6wceq 1474 1 wff (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
Colors of variables: wff setvar class
This definition is referenced by:  reseq1  5297  reseq2  5298  nfres  5305  csbres  5306  res0  5307  opelres  5308  resres  5315  resundi  5316  resundir  5317  resindi  5318  resindir  5319  inres  5320  resdifcom  5321  resiun1  5322  resiun1OLD  5323  resiun2  5324  resss  5328  ssres  5330  ssres2  5331  relres  5332  xpssres  5340  resopab  5352  ssrnres  5476  imainrect  5479  xpima  5480  cnvcnv2  5491  resdmres  5528  ressnop0  6302  fndifnfp  6324  tpres  6348  marypha1lem  8199  gsum2d  18142  gsumxp  18146  pjdm  19817  hausdiag  21205  isngp2  22158  ovoliunlem1  23021  xpdisjres  28586  difres  28588  imadifxp  28589  mbfmcst  29441  0rrv  29633  dfres3  30695  elrn3  30699  dfon4  30963  restrreld  36761  csbresgOLD  37860  csbresgVD  37936
  Copyright terms: Public domain W3C validator