This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem undi

Description: Distributive law for union over intersection. Exercise 11 of TakeutiZaring p. 17. (Contributed by NM, 30-Sep-2002) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion undi ( 𝐴 ∪ ( 𝐵 ∩ 𝐶 ) ) = ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐴 ∪ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 elin ⊢ ( 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) )
2 1 orbi2i ⊢ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) )
3 ordi ⊢ ( ( 𝑥 ∈ 𝐴 ∨ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶 ) ) )
4 elin ⊢ ( 𝑥 ∈ ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐴 ∪ 𝐶 ) ) ↔ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 ∪ 𝐶 ) ) )
5 elun ⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
6 elun ⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶 ) )
7 5 6 anbi12i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 ∪ 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶 ) ) )
8 4 7 bitr2i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶 ) ) ↔ 𝑥 ∈ ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐴 ∪ 𝐶 ) ) )
9 2 3 8 3bitri ⊢ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ) ↔ 𝑥 ∈ ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐴 ∪ 𝐶 ) ) )
10 9 uneqri ⊢ ( 𝐴 ∪ ( 𝐵 ∩ 𝐶 ) ) = ( ( 𝐴 ∪ 𝐵 ) ∩ ( 𝐴 ∪ 𝐶 ) )