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

Theorem resres 5587
Description: The restriction of a restriction. (Contributed by NM, 27-Mar-2008.)
Assertion
Ref Expression
resres ((𝐴𝐵) ↾ 𝐶) = (𝐴 ↾ (𝐵𝐶))

Proof of Theorem resres
StepHypRef Expression
1 df-res 5291 . 2 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐵) ∩ (𝐶 × V))
2 df-res 5291 . . 3 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
32ineq1i 3974 . 2 ((𝐴𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V))
4 xpindir 5427 . . . 4 ((𝐵𝐶) × V) = ((𝐵 × V) ∩ (𝐶 × V))
54ineq2i 3975 . . 3 (𝐴 ∩ ((𝐵𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∩ (𝐶 × V)))
6 df-res 5291 . . 3 (𝐴 ↾ (𝐵𝐶)) = (𝐴 ∩ ((𝐵𝐶) × V))
7 inass 3985 . . 3 ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V)) = (𝐴 ∩ ((𝐵 × V) ∩ (𝐶 × V)))
85, 6, 73eqtr4ri 2798 . 2 ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V)) = (𝐴 ↾ (𝐵𝐶))
91, 3, 83eqtri 2791 1 ((𝐴𝐵) ↾ 𝐶) = (𝐴 ↾ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1652  Vcvv 3350  cin 3733   × cxp 5277  cres 5281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pr 5064
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rab 3064  df-v 3352  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-opab 4874  df-xp 5285  df-rel 5286  df-res 5291
This theorem is referenced by:  rescom  5600  resabs1  5604  resima2  5609  resmpt3  5629  resdisj  5748  rescnvcnv  5782  fresin  6257  resdif  6344  curry1  7475  curry2  7478  wfrlem4  7625  wfrlem4OLD  7626  pmresg  8092  gruima  9881  rlimres  14588  lo1res  14589  rlimresb  14595  lo1eq  14598  rlimeq  14599  fsets  16178  setsid  16200  sscres  16762  gsumzres  18590  txkgen  21749  tsmsres  22240  ressxms  22623  ressms  22624  dvres  23980  dvres3a  23983  cpnres  24005  dvmptres3  24024  rlimcnp2  24998  df1stres  29951  df2ndres  29952  indf1ofs  30556  frrlem4  32248  dfrcl2  38665  relexpaddss  38709  limsupresuz  40597  liminfresuz  40678  fouriersw  41109  fouriercn  41110
  Copyright terms: Public domain W3C validator