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

Theorem indir 4010
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 4008 . 2 (𝐶 ∩ (𝐴𝐵)) = ((𝐶𝐴) ∪ (𝐶𝐵))
2 incom 3940 . 2 ((𝐴𝐵) ∩ 𝐶) = (𝐶 ∩ (𝐴𝐵))
3 incom 3940 . . 3 (𝐴𝐶) = (𝐶𝐴)
4 incom 3940 . . 3 (𝐵𝐶) = (𝐶𝐵)
53, 4uneq12i 3900 . 2 ((𝐴𝐶) ∪ (𝐵𝐶)) = ((𝐶𝐴) ∪ (𝐶𝐵))
61, 2, 53eqtr4i 2784 1 ((𝐴𝐵) ∩ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1624  cun 3705  cin 3706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-v 3334  df-un 3712  df-in 3714
This theorem is referenced by:  difundir  4015  undisj1  4165  disjpr2  4384  disjpr2OLD  4385  resundir  5561  predun  5857  cdaassen  9188  fin23lem26  9331  fpwwe2lem13  9648  neitr  21178  fiuncmp  21401  connsuba  21417  trfil2  21884  tsmsres  22140  trust  22226  restmetu  22568  volun  23505  uniioombllem3  23545  itgsplitioo  23795  ppiprm  25068  chtprm  25070  chtdif  25075  ppidif  25080  carsgclctunlem1  30680  ballotlemfp1  30854  ballotlemgun  30887  mrsubvrs  31718  mthmpps  31778  fixun  32314  mbfposadd  33762  iunrelexp0  38488  31prm  42014
  Copyright terms: Public domain W3C validator