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

Metamath Proof Explorer

Theorem uniun

Description: The class union of the union of two classes. Theorem 8.3 of Quine p. 53. (Contributed by NM, 20-Aug-1993)

Ref Expression
Assertion uniun ∪ ( 𝐴 ∪ 𝐵 ) = ( ∪ 𝐴 ∪ ∪ 𝐵 )

Proof

Step Hyp Ref Expression
1 19.43 ⊢ ( ∃ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ∨ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) ↔ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ∨ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) )
2 elun ⊢ ( 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵 ) )
3 2 anbi2i ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵 ) ) )
4 andi ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵 ) ) ↔ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ∨ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) )
5 3 4 bitri ⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ) ↔ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ∨ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) )
6 5 exbii ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ) ↔ ∃ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ∨ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) )
7 eluni ⊢ ( 𝑥 ∈ ∪ 𝐴 ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) )
8 eluni ⊢ ( 𝑥 ∈ ∪ 𝐵 ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) )
9 7 8 orbi12i ⊢ ( ( 𝑥 ∈ ∪ 𝐴 ∨ 𝑥 ∈ ∪ 𝐵 ) ↔ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ∨ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) )
10 1 6 9 3bitr4i ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ) ↔ ( 𝑥 ∈ ∪ 𝐴 ∨ 𝑥 ∈ ∪ 𝐵 ) )
11 eluni ⊢ ( 𝑥 ∈ ∪ ( 𝐴 ∪ 𝐵 ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ) )
12 elun ⊢ ( 𝑥 ∈ ( ∪ 𝐴 ∪ ∪ 𝐵 ) ↔ ( 𝑥 ∈ ∪ 𝐴 ∨ 𝑥 ∈ ∪ 𝐵 ) )
13 10 11 12 3bitr4i ⊢ ( 𝑥 ∈ ∪ ( 𝐴 ∪ 𝐵 ) ↔ 𝑥 ∈ ( ∪ 𝐴 ∪ ∪ 𝐵 ) )
14 13 eqriv ⊢ ∪ ( 𝐴 ∪ 𝐵 ) = ( ∪ 𝐴 ∪ ∪ 𝐵 )