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

Theorem indir 3834
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 3832 . 2 (𝐶 ∩ (𝐴𝐵)) = ((𝐶𝐴) ∪ (𝐶𝐵))
2 incom 3767 . 2 ((𝐴𝐵) ∩ 𝐶) = (𝐶 ∩ (𝐴𝐵))
3 incom 3767 . . 3 (𝐴𝐶) = (𝐶𝐴)
4 incom 3767 . . 3 (𝐵𝐶) = (𝐶𝐵)
53, 4uneq12i 3727 . 2 ((𝐴𝐶) ∪ (𝐵𝐶)) = ((𝐶𝐴) ∪ (𝐶𝐵))
61, 2, 53eqtr4i 2642 1 ((𝐴𝐵) ∩ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475  cun 3538  cin 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547
This theorem is referenced by:  difundir  3839  undisj1  3981  disjpr2  4194  disjpr2OLD  4195  resundir  5318  predun  5607  cdaassen  8865  fin23lem26  9008  fpwwe2lem13  9321  neitr  20742  fiuncmp  20965  consuba  20981  trfil2  21449  tsmsres  21705  trust  21791  restmetu  22133  volun  23065  uniioombllem3  23104  itgsplitioo  23355  ppiprm  24622  chtprm  24624  chtdif  24629  ppidif  24634  carsgclctunlem1  29500  ballotlemfp1  29674  ballotlemgun  29707  mrsubvrs  30467  mthmpps  30527  fixun  30980  mbfposadd  32421  iunrelexp0  36807  31prm  39845
  Copyright terms: Public domain W3C validator