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.

Step	Hyp	Ref	Expression
1		andi 1007	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶)))
2		elin 3963	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
3		elin 3963	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))
4	2, 3	orbi12i 914	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∩ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶)))
5	1, 4	bitr4i 278	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) ↔ (𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∩ 𝐶)))
6		elun 4147	. . . 4 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
7	6	anbi2i 624	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
8		elun 4147	. . 3 ⊢ (𝑥 ∈ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶)) ↔ (𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∩ 𝐶)))
9	5, 7, 8	3bitr4i 303	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ 𝑥 ∈ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶)))
10	9	ineqri 4203	1 ⊢ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶))

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