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

Theorem indir 3908
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 3906 . 2 (𝐶 ∩ (𝐴𝐵)) = ((𝐶𝐴) ∪ (𝐶𝐵))
2 incom 3838 . 2 ((𝐴𝐵) ∩ 𝐶) = (𝐶 ∩ (𝐴𝐵))
3 incom 3838 . . 3 (𝐴𝐶) = (𝐶𝐴)
4 incom 3838 . . 3 (𝐵𝐶) = (𝐶𝐵)
53, 4uneq12i 3798 . 2 ((𝐴𝐶) ∪ (𝐵𝐶)) = ((𝐶𝐴) ∪ (𝐶𝐵))
61, 2, 53eqtr4i 2683 1 ((𝐴𝐵) ∩ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  cun 3605  cin 3606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-in 3614
This theorem is referenced by:  difundir  3913  undisj1  4062  disjpr2  4280  disjpr2OLD  4281  resundir  5446  predun  5742  cdaassen  9042  fin23lem26  9185  fpwwe2lem13  9502  neitr  21032  fiuncmp  21255  connsuba  21271  trfil2  21738  tsmsres  21994  trust  22080  restmetu  22422  volun  23359  uniioombllem3  23399  itgsplitioo  23649  ppiprm  24922  chtprm  24924  chtdif  24929  ppidif  24934  carsgclctunlem1  30507  ballotlemfp1  30681  ballotlemgun  30714  mrsubvrs  31545  mthmpps  31605  fixun  32141  mbfposadd  33587  iunrelexp0  38311  31prm  41837
  Copyright terms: Public domain W3C validator