Theorem indi 4237

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 1010	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶)))
2		elin 3918	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
3		elin 3918	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))
4	2, 3	orbi12i 915	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∩ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶)))
5	1, 4	bitr4i 278	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) ↔ (𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∩ 𝐶)))
6		elun 4106	. . . 4 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
7	6	anbi2i 624	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
8		elun 4106	. . 3 ⊢ (𝑥 ∈ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶)) ↔ (𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∩ 𝐶)))
9	5, 7, 8	3bitr4i 303	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 ∪ 𝐶)) ↔ 𝑥 ∈ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶)))
10	9	ineqri 4165	1 ⊢ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶))

Syntax hints:   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ∪ cun 3900   ∩ cin 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-un 3907  df-in 3909

This theorem is referenced by:  indir  4239  difindi  4245  undisj2  4416  disjssun  4421  difdifdir  4445  disjpr2  4671  resundi  5953  fresaun  6706  elfiun  9337  unxpwdom  9498  kmlem2  10066  djuinf  10103  ackbij1lem1  10133  ackbij1lem2  10134  ssxr  11206  incexclem  15763  bitsinv1  16373  bitsinvp1  16380  bitsres  16404  paste  23242  unmbl  25498  ovolioo  25529  uniioombllem4  25547  volcn  25567  ellimc2  25838  lhop2  25980  ex-in  30504  eulerpartgbij  34531  poimirlem3  37826  poimirlem15  37838  asindmre  37906  iunrelexp0  44010  sge0resplit  46717  sge0split  46720  tposresg  49190  tposrescnv  49191  iscnrm3rlem1  49252  topdlat  49316