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

Theorem indi 3832
 Description: Distributive law for intersection over union. Exercise 10 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
indi (𝐴 ∩ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))

Proof of Theorem indi
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 andi 907 . . . 4 ((𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)) ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴𝑥𝐶)))
2 elin 3758 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
3 elin 3758 . . . . 5 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
42, 3orbi12i 542 . . . 4 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐶)) ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴𝑥𝐶)))
51, 4bitr4i 266 . . 3 ((𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)) ↔ (𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐶)))
6 elun 3715 . . . 4 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
76anbi2i 726 . . 3 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
8 elun 3715 . . 3 (𝑥 ∈ ((𝐴𝐵) ∪ (𝐴𝐶)) ↔ (𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐶)))
95, 7, 83bitr4i 291 . 2 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ 𝑥 ∈ ((𝐴𝐵) ∪ (𝐴𝐶)))
109ineqri 3768 1 (𝐴 ∩ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))
 Colors of variables: wff setvar class Syntax hints:   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ∪ cun 3538   ∩ cin 3539 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547 This theorem is referenced by:  indir  3834  difindi  3840  undisj2  3982  disjssun  3988  difdifdir  4008  disjpr2  4194  disjpr2OLD  4195  diftpsn3OLD  4274  resundi  5330  fresaun  5988  elfiun  8219  unxpwdom  8377  kmlem2  8856  cdainf  8897  ackbij1lem1  8925  ackbij1lem2  8926  ssxr  9986  incexclem  14407  bitsinv1  15002  bitsinvp1  15009  bitsres  15033  paste  20908  unmbl  23112  ovolioo  23143  uniioombllem4  23160  volcn  23180  ellimc2  23447  lhop2  23582  ex-in  26674  eulerpartgbij  29761  poimirlem3  32582  poimirlem15  32594  asindmre  32665  iunrelexp0  37013  sge0resplit  39299  sge0split  39302
 Copyright terms: Public domain W3C validator