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 5270
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 15041) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 14989 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 27601). (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 5260 . 2 class (𝐴𝐵)
4 cvv 3332 . . . 4 class V
52, 4cxp 5256 . . 3 class (𝐵 × V)
61, 5cin 3706 . 2 class (𝐴 ∩ (𝐵 × V))
73, 6wceq 1624 1 wff (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
Colors of variables: wff setvar class
This definition is referenced by:  reseq1  5537  reseq2  5538  nfres  5545  csbres  5546  res0  5547  dfres3  5548  opelresg  5549  opelresOLD  5553  resres  5559  resundi  5560  resundir  5561  resindi  5562  resindir  5563  inres  5564  resdifcom  5565  resiun1  5566  resiun1OLD  5567  resiun2  5568  resss  5572  ssres  5574  ssres2  5575  relres  5576  xpssres  5584  resopab  5596  ssrnres  5722  imainrect  5725  xpima  5726  cnvcnv2  5738  resdmres  5778  ressnop0  6575  fndifnfp  6598  tpres  6622  marypha1lem  8496  gsum2d  18563  gsumxp  18567  pjdm  20245  hausdiag  21642  isngp2  22594  ovoliunlem1  23462  xpdisjres  29710  difres  29712  imadifxp  29713  mbfmcst  30622  0rrv  30814  elrn3  31951  nosupbnd2lem1  32159  noetalem2  32162  noetalem3  32163  dfon4  32298  opelresALTV  34347  inxpssres  34392  restrreld  38453  csbresgOLD  39547  csbresgVD  39622
  Copyright terms: Public domain W3C validator