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 4183 . 2 ((𝐴𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V))
4 xpindir 5698 . . . 4 ((𝐵𝐶) × V) = ((𝐵 × V) ∩ (𝐶 × V))
54ineq2i 4184 . . 3 (𝐴 ∩ ((𝐵𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∩ (𝐶 × V)))
6 df-res 5560 . . 3 (𝐴 ↾ (𝐵𝐶)) = (𝐴 ∩ ((𝐵𝐶) × V))
7 inass 4194 . . 3 ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V)) = (𝐴 ∩ ((𝐵 × V) ∩ (𝐶 × V)))
85, 6, 73eqtr4ri 2853 . 2 ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V)) = (𝐴 ↾ (𝐵𝐶))
91, 3, 83eqtri 2846 1 ((𝐴𝐵) ↾ 𝐶) = (𝐴 ↾ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  Vcvv 3493  cin 3933   × cxp 5546  cres 5550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  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  7791  curry2  7794  wfrlem4  7950  pmresg  8426  gruima  10216  rlimres  14907  lo1res  14908  rlimresb  14914  lo1eq  14917  rlimeq  14918  fsets  16508  setsid  16530  sscres  17085  gsumzres  19021  txkgen  22252  tsmsres  22744  ressxms  23127  ressms  23128  dvres  24501  dvres3a  24504  cpnres  24526  dvmptres3  24545  rlimcnp2  25536  df1stres  30431  df2ndres  30432  indf1ofs  31273  frrlem4  33114  dfrcl2  40004  relexpaddss  40048  limsupresuz  41968  liminfresuz  42049  fouriersw  42501  fouriercn  42502
  Copyright terms: Public domain W3C validator