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

Theorem resres 5859
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 5560 . 2 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐵) ∩ (𝐶 × V))
2 df-res 5560 . . 3 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
32ineq1i 4182 . 2 ((𝐴𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V))
4 xpindir 5698 . . . 4 ((𝐵𝐶) × V) = ((𝐵 × V) ∩ (𝐶 × V))
54ineq2i 4183 . . 3 (𝐴 ∩ ((𝐵𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∩ (𝐶 × V)))
6 df-res 5560 . . 3 (𝐴 ↾ (𝐵𝐶)) = (𝐴 ∩ ((𝐵𝐶) × V))
7 inass 4193 . . 3 ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V)) = (𝐴 ∩ ((𝐵 × V) ∩ (𝐶 × V)))
85, 6, 73eqtr4ri 2852 . 2 ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V)) = (𝐴 ↾ (𝐵𝐶))
91, 3, 83eqtri 2845 1 ((𝐴𝐵) ↾ 𝐶) = (𝐴 ↾ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  Vcvv 3492  cin 3932   × cxp 5546  cres 5550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-opab 5120  df-xp 5554  df-rel 5555  df-res 5560
This theorem is referenced by:  rescom  5872  resabs1  5876  resima2  5881  resmpt3  5899  resdisj  6019  rescnvcnv  6054  fresin  6540  resdif  6628  curry1  7788  curry2  7791  wfrlem4  7947  pmresg  8423  gruima  10212  rlimres  14903  lo1res  14904  rlimresb  14910  lo1eq  14913  rlimeq  14914  fsets  16504  setsid  16526  sscres  17081  gsumzres  18958  txkgen  22188  tsmsres  22679  ressxms  23062  ressms  23063  dvres  24436  dvres3a  24439  cpnres  24461  dvmptres3  24480  rlimcnp2  25471  df1stres  30365  df2ndres  30366  indf1ofs  31184  frrlem4  33023  dfrcl2  39897  relexpaddss  39941  limsupresuz  41860  liminfresuz  41941  fouriersw  42393  fouriercn  42394
  Copyright terms: Public domain W3C validator