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

Theorem indir 4276
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 4274 . 2 (𝐶 ∩ (𝐴𝐵)) = ((𝐶𝐴) ∪ (𝐶𝐵))
2 incom 4202 . 2 ((𝐴𝐵) ∩ 𝐶) = (𝐶 ∩ (𝐴𝐵))
3 incom 4202 . . 3 (𝐴𝐶) = (𝐶𝐴)
4 incom 4202 . . 3 (𝐵𝐶) = (𝐶𝐵)
53, 4uneq12i 4162 . 2 ((𝐴𝐶) ∪ (𝐵𝐶)) = ((𝐶𝐴) ∪ (𝐶𝐵))
61, 2, 53eqtr4i 2771 1 ((𝐴𝐵) ∩ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cun 3947  cin 3948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-un 3954  df-in 3956
This theorem is referenced by:  difundir  4281  undisj1  4462  disjpr2  4718  resundir  5997  predun  6330  djuassen  10173  fin23lem26  10320  fpwwe2lem12  10637  neitr  22684  fiuncmp  22908  connsuba  22924  trfil2  23391  tsmsres  23648  trust  23734  restmetu  24079  volun  25062  uniioombllem3  25102  itgsplitioo  25355  ppiprm  26655  chtprm  26657  chtdif  26662  ppidif  26667  cycpmco2f1  32283  carsgclctunlem1  33316  ballotlemfp1  33490  ballotlemgun  33523  mrsubvrs  34513  mthmpps  34573  fixun  34881  mbfposadd  36535  metakunt17  41001  metakunt21  41005  metakunt22  41006  metakunt24  41008  iunrelexp0  42453  31prm  46265
  Copyright terms: Public domain W3C validator