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

Theorem indir 4286
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 4284 . 2 (𝐶 ∩ (𝐴𝐵)) = ((𝐶𝐴) ∪ (𝐶𝐵))
2 incom 4209 . 2 ((𝐴𝐵) ∩ 𝐶) = (𝐶 ∩ (𝐴𝐵))
3 incom 4209 . . 3 (𝐴𝐶) = (𝐶𝐴)
4 incom 4209 . . 3 (𝐵𝐶) = (𝐶𝐵)
53, 4uneq12i 4166 . 2 ((𝐴𝐶) ∪ (𝐵𝐶)) = ((𝐶𝐴) ∪ (𝐶𝐵))
61, 2, 53eqtr4i 2775 1 ((𝐴𝐵) ∩ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  cun 3949  cin 3950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-un 3956  df-in 3958
This theorem is referenced by:  difundir  4291  undisj1  4462  disjpr2  4713  resundir  6012  predun  6349  djuassen  10219  fin23lem26  10365  fpwwe2lem12  10682  neitr  23188  fiuncmp  23412  connsuba  23428  trfil2  23895  tsmsres  24152  trust  24238  restmetu  24583  volun  25580  uniioombllem3  25620  itgsplitioo  25873  ppiprm  27194  chtprm  27196  chtdif  27201  ppidif  27206  cycpmco2f1  33144  carsgclctunlem1  34319  ballotlemfp1  34494  ballotlemgun  34527  mrsubvrs  35527  mthmpps  35587  fixun  35910  mbfposadd  37674  metakunt17  42222  metakunt21  42226  metakunt22  42227  metakunt24  42229  iunrelexp0  43715  31prm  47584
  Copyright terms: Public domain W3C validator