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

Theorem resundi 5994
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 5744 . . . 4 ((𝐵𝐶) × V) = ((𝐵 × V) ∪ (𝐶 × V))
21ineq2i 4208 . . 3 (𝐴 ∩ ((𝐵𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V)))
3 indi 4272 . . 3 (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V))) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
42, 3eqtri 2758 . 2 (𝐴 ∩ ((𝐵𝐶) × V)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
5 df-res 5687 . 2 (𝐴 ↾ (𝐵𝐶)) = (𝐴 ∩ ((𝐵𝐶) × V))
6 df-res 5687 . . 3 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
7 df-res 5687 . . 3 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
86, 7uneq12i 4160 . 2 ((𝐴𝐵) ∪ (𝐴𝐶)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
94, 5, 83eqtr4i 2768 1 (𝐴 ↾ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1539  Vcvv 3472  cun 3945  cin 3946   × cxp 5673  cres 5677
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-un 3952  df-in 3954  df-opab 5210  df-xp 5681  df-res 5687
This theorem is referenced by:  reldisjun  6031  imaundi  6148  relresfld  6274  resasplit  6760  fresaunres2  6762  residpr  7142  fnsnsplit  7183  eqfunresadj  7359  tfrlem16  8395  mapunen  9148  fnfi  9183  fseq1p1m1  13579  resunimafz0  14408  gsum2dlem2  19880  dprd2da  19953  evlseu  21865  ptuncnv  23531  mbfres2  25394  nosupbnd2lem1  27454  noinfbnd2lem1  27469  ffsrn  32221  resf1o  32222  symgcom  32514  tocyc01  32547  cvmliftlem10  34583  poimirlem9  36800  disjresundif  37412  eldioph4b  41851  pwssplit4  42133  tfsconcatrev  42400  undmrnresiss  42657  relexp0a  42769  rnresun  44177
  Copyright terms: Public domain W3C validator