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

Theorem indi 4272
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 1007 . . . 4 ((𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)) ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴𝑥𝐶)))
2 elin 3963 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
3 elin 3963 . . . . 5 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴𝑥𝐶))
42, 3orbi12i 914 . . . 4 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐶)) ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴𝑥𝐶)))
51, 4bitr4i 278 . . 3 ((𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)) ↔ (𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐶)))
6 elun 4147 . . . 4 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
76anbi2i 624 . . 3 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
8 elun 4147 . . 3 (𝑥 ∈ ((𝐴𝐵) ∪ (𝐴𝐶)) ↔ (𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐶)))
95, 7, 83bitr4i 303 . 2 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ 𝑥 ∈ ((𝐴𝐵) ∪ (𝐴𝐶)))
109ineqri 4203 1 (𝐴 ∩ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 397  wo 846   = wceq 1542  wcel 2107  cun 3945  cin 3946
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-v 3477  df-un 3952  df-in 3954
This theorem is referenced by:  indir  4274  difindi  4280  undisj2  4461  disjssun  4466  difdifdir  4490  disjpr2  4716  resundi  5993  fresaun  6759  elfiun  9421  unxpwdom  9580  kmlem2  10142  djuinf  10179  ackbij1lem1  10211  ackbij1lem2  10212  ssxr  11279  incexclem  15778  bitsinv1  16379  bitsinvp1  16386  bitsres  16410  paste  22780  unmbl  25036  ovolioo  25067  uniioombllem4  25085  volcn  25105  ellimc2  25376  lhop2  25514  ex-in  29658  eulerpartgbij  33309  poimirlem3  36429  poimirlem15  36441  asindmre  36509  iunrelexp0  42386  sge0resplit  45057  sge0split  45060  iscnrm3rlem1  47475  topdlat  47531
  Copyright terms: Public domain W3C validator