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

Theorem indir 4256
 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 4254 . 2 (𝐶 ∩ (𝐴𝐵)) = ((𝐶𝐴) ∪ (𝐶𝐵))
2 incom 4182 . 2 ((𝐴𝐵) ∩ 𝐶) = (𝐶 ∩ (𝐴𝐵))
3 incom 4182 . . 3 (𝐴𝐶) = (𝐶𝐴)
4 incom 4182 . . 3 (𝐵𝐶) = (𝐶𝐵)
53, 4uneq12i 4141 . 2 ((𝐴𝐶) ∪ (𝐵𝐶)) = ((𝐶𝐴) ∪ (𝐶𝐵))
61, 2, 53eqtr4i 2859 1 ((𝐴𝐵) ∩ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   = wceq 1530   ∪ cun 3938   ∩ cin 3939 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rab 3152  df-v 3502  df-un 3945  df-in 3947 This theorem is referenced by:  difundir  4261  undisj1  4414  disjpr2  4648  resundir  5867  predun  6171  djuassen  9598  fin23lem26  9741  fpwwe2lem13  10058  neitr  21723  fiuncmp  21947  connsuba  21963  trfil2  22430  tsmsres  22686  trust  22772  restmetu  23114  volun  24080  uniioombllem3  24120  itgsplitioo  24372  ppiprm  25661  chtprm  25663  chtdif  25668  ppidif  25673  cycpmco2f1  30699  carsgclctunlem1  31480  ballotlemfp1  31654  ballotlemgun  31687  mrsubvrs  32672  mthmpps  32732  fixun  33273  mbfposadd  34825  iunrelexp0  39931  31prm  43611
 Copyright terms: Public domain W3C validator