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

Metamath Proof Explorer

Theorem uniin

Description: The class union of the intersection of two classes. Exercise 4.12(n) of Mendelson p. 235. See uniinqs for a condition where equality holds. (Contributed by NM, 4-Dec-2003) (Proof shortened by Andrew Salmon, 29-Jun-2011)

Ref Expression
Assertion uniin ∪ ( 𝐴 ∩ 𝐵 ) ⊆ ( ∪ 𝐴 ∩ ∪ 𝐵 )

Proof

Step Hyp Ref Expression
1 19.40 ⊢ ( ∃ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) )
2 elin ⊢ ( 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
3 2 anbi2i ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
4 anandi ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ↔ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) )
5 3 4 bitri ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) )
6 5 exbii ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ↔ ∃ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) )
7 eluni ⊢ ( 𝑥 ∈ ∪ 𝐴 ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) )
8 eluni ⊢ ( 𝑥 ∈ ∪ 𝐵 ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) )
9 7 8 anbi12i ⊢ ( ( 𝑥 ∈ ∪ 𝐴 ∧ 𝑥 ∈ ∪ 𝐵 ) ↔ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) )
10 1 6 9 3imtr4i ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( 𝑥 ∈ ∪ 𝐴 ∧ 𝑥 ∈ ∪ 𝐵 ) )
11 eluni ⊢ ( 𝑥 ∈ ∪ ( 𝐴 ∩ 𝐵 ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) )
12 elin ⊢ ( 𝑥 ∈ ( ∪ 𝐴 ∩ ∪ 𝐵 ) ↔ ( 𝑥 ∈ ∪ 𝐴 ∧ 𝑥 ∈ ∪ 𝐵 ) )
13 10 11 12 3imtr4i ⊢ ( 𝑥 ∈ ∪ ( 𝐴 ∩ 𝐵 ) → 𝑥 ∈ ( ∪ 𝐴 ∩ ∪ 𝐵 ) )
14 13 ssriv ⊢ ∪ ( 𝐴 ∩ 𝐵 ) ⊆ ( ∪ 𝐴 ∩ ∪ 𝐵 )