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

Theorem resundi 5865
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 5618 . . . 4 ((𝐵𝐶) × V) = ((𝐵 × V) ∪ (𝐶 × V))
21ineq2i 4124 . . 3 (𝐴 ∩ ((𝐵𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V)))
3 indi 4188 . . 3 (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V))) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
42, 3eqtri 2765 . 2 (𝐴 ∩ ((𝐵𝐶) × V)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
5 df-res 5563 . 2 (𝐴 ↾ (𝐵𝐶)) = (𝐴 ∩ ((𝐵𝐶) × V))
6 df-res 5563 . . 3 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
7 df-res 5563 . . 3 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
86, 7uneq12i 4075 . 2 ((𝐴𝐵) ∪ (𝐴𝐶)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
94, 5, 83eqtr4i 2775 1 (𝐴 ↾ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543  Vcvv 3408  cun 3864  cin 3865   × cxp 5549  cres 5553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-un 3871  df-in 3873  df-opab 5116  df-xp 5557  df-res 5563
This theorem is referenced by:  imaundi  6013  relresfld  6139  resasplit  6589  fresaunres2  6591  residpr  6958  fnsnsplit  6999  tfrlem16  8129  mapunen  8815  fnfi  8858  fseq1p1m1  13186  resunimafz0  14009  gsum2dlem2  19356  dprd2da  19429  evlseu  21043  ptuncnv  22704  mbfres2  24542  reldisjun  30661  ffsrn  30784  resf1o  30785  symgcom  31071  tocyc01  31104  cvmliftlem10  32969  eqfunresadj  33454  nosupbnd2lem1  33655  noinfbnd2lem1  33670  poimirlem9  35523  eldioph4b  40336  pwssplit4  40617  undmrnresiss  40888  relexp0a  41001  rnresun  42389
  Copyright terms: Public domain W3C validator