Theorem indi 4174

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 1002	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶)))
2		elin 4094	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
3		elin 4094	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))
4	2, 3	orbi12i 909	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∩ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶)))
5	1, 4	bitr4i 279	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) ↔ (𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∩ 𝐶)))
6		elun 4050	. . . 4 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
7	6	anbi2i 622	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
8		elun 4050	. . 3 ⊢ (𝑥 ∈ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶)) ↔ (𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∩ 𝐶)))
9	5, 7, 8	3bitr4i 304	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ 𝑥 ∈ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶)))
10	9	ineqri 4104	1 ⊢ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶))

Syntax hints:   ∧ wa 396   ∨ wo 842   = wceq 1522   ∈ wcel 2081   ∪ cun 3861   ∩ cin 3862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-un 3868  df-in 3870

This theorem is referenced by:  indir  4176  difindi  4182  undisj2  4330  disjssun  4335  difdifdir  4355  disjpr2  4560  resundi  5753  fresaun  6422  elfiun  8745  unxpwdom  8904  kmlem2  9428  djuinf  9465  ackbij1lem1  9493  ackbij1lem2  9494  ssxr  10562  incexclem  15029  bitsinv1  15629  bitsinvp1  15636  bitsres  15660  paste  21591  unmbl  23826  ovolioo  23857  uniioombllem4  23875  volcn  23895  ellimc2  24163  lhop2  24300  ex-in  27901  eulerpartgbij  31252  poimirlem3  34451  poimirlem15  34463  asindmre  34533  iunrelexp0  39557  sge0resplit  42256  sge0split  42259