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

Theorem resundi 5833
 Description: Distributive law for restriction over union. Theorem 31 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.)
Assertion
Ref Expression
resundi (𝐴 ↾ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))

Proof of Theorem resundi
StepHypRef Expression
1 xpundir 5586 . . . 4 ((𝐵𝐶) × V) = ((𝐵 × V) ∪ (𝐶 × V))
21ineq2i 4136 . . 3 (𝐴 ∩ ((𝐵𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V)))
3 indi 4200 . . 3 (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V))) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
42, 3eqtri 2821 . 2 (𝐴 ∩ ((𝐵𝐶) × V)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
5 df-res 5532 . 2 (𝐴 ↾ (𝐵𝐶)) = (𝐴 ∩ ((𝐵𝐶) × V))
6 df-res 5532 . . 3 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
7 df-res 5532 . . 3 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
86, 7uneq12i 4088 . 2 ((𝐴𝐵) ∪ (𝐴𝐶)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
94, 5, 83eqtr4i 2831 1 (𝐴 ↾ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538  Vcvv 3441   ∪ cun 3879   ∩ cin 3880   × cxp 5518   ↾ cres 5522 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-opab 5094  df-xp 5526  df-res 5532 This theorem is referenced by:  imaundi  5976  relresfld  6096  resasplit  6523  fresaunres2  6525  residpr  6883  fnsnsplit  6924  tfrlem16  8015  mapunen  8673  fnfi  8783  fseq1p1m1  12979  resunimafz0  13802  gsum2dlem2  19088  dprd2da  19161  evlseu  20761  ptuncnv  22422  mbfres2  24259  reldisjun  30376  ffsrn  30501  resf1o  30502  symgcom  30787  tocyc01  30820  cvmliftlem10  32669  eqfunresadj  33132  nosupbnd2lem1  33343  poimirlem9  35085  eldioph4b  39795  pwssplit4  40076  undmrnresiss  40347  relexp0a  40460  rnresun  41847
 Copyright terms: Public domain W3C validator