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

Theorem indir 4249
Description: Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
Assertion
Ref Expression
indir ((𝐴𝐵) ∩ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))

Proof of Theorem indir
StepHypRef Expression
1 indi 4247 . 2 (𝐶 ∩ (𝐴𝐵)) = ((𝐶𝐴) ∪ (𝐶𝐵))
2 incom 4175 . 2 ((𝐴𝐵) ∩ 𝐶) = (𝐶 ∩ (𝐴𝐵))
3 incom 4175 . . 3 (𝐴𝐶) = (𝐶𝐴)
4 incom 4175 . . 3 (𝐵𝐶) = (𝐶𝐵)
53, 4uneq12i 4134 . 2 ((𝐴𝐶) ∪ (𝐵𝐶)) = ((𝐶𝐴) ∪ (𝐶𝐵))
61, 2, 53eqtr4i 2851 1 ((𝐴𝐵) ∩ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  cun 3931  cin 3932
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
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  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-un 3938  df-in 3940
This theorem is referenced by:  difundir  4254  undisj1  4407  disjpr2  4641  resundir  5861  predun  6165  djuassen  9592  fin23lem26  9735  fpwwe2lem13  10052  neitr  21716  fiuncmp  21940  connsuba  21956  trfil2  22423  tsmsres  22679  trust  22765  restmetu  23107  volun  24073  uniioombllem3  24113  itgsplitioo  24365  ppiprm  25655  chtprm  25657  chtdif  25662  ppidif  25667  cycpmco2f1  30693  carsgclctunlem1  31474  ballotlemfp1  31648  ballotlemgun  31681  mrsubvrs  32666  mthmpps  32726  fixun  33267  mbfposadd  34820  iunrelexp0  39925  31prm  43637
  Copyright terms: Public domain W3C validator