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 ⊢ ⋃ A ∪ B = ⋃ A ∪ ⋃ B

Proof

Step Hyp Ref Expression
1 19.43 ⊢ ∃ y x ∈ y ∧ y ∈ A ∨ x ∈ y ∧ y ∈ B ↔ ∃ y x ∈ y ∧ y ∈ A ∨ ∃ y x ∈ y ∧ y ∈ B
2 elun ⊢ y ∈ A ∪ B ↔ y ∈ A ∨ y ∈ B
3 2 anbi2i ⊢ x ∈ y ∧ y ∈ A ∪ B ↔ x ∈ y ∧ y ∈ A ∨ y ∈ B
4 andi ⊢ x ∈ y ∧ y ∈ A ∨ y ∈ B ↔ x ∈ y ∧ y ∈ A ∨ x ∈ y ∧ y ∈ B
5 3 4 bitri ⊢ x ∈ y ∧ y ∈ A ∪ B ↔ x ∈ y ∧ y ∈ A ∨ x ∈ y ∧ y ∈ B
6 5 exbii ⊢ ∃ y x ∈ y ∧ y ∈ A ∪ B ↔ ∃ y x ∈ y ∧ y ∈ A ∨ x ∈ y ∧ y ∈ B
7 eluni ⊢ x ∈ ⋃ A ↔ ∃ y x ∈ y ∧ y ∈ A
8 eluni ⊢ x ∈ ⋃ B ↔ ∃ y x ∈ y ∧ y ∈ B
9 7 8 orbi12i ⊢ x ∈ ⋃ A ∨ x ∈ ⋃ B ↔ ∃ y x ∈ y ∧ y ∈ A ∨ ∃ y x ∈ y ∧ y ∈ B
10 1 6 9 3bitr4i ⊢ ∃ y x ∈ y ∧ y ∈ A ∪ B ↔ x ∈ ⋃ A ∨ x ∈ ⋃ B
11 eluni ⊢ x ∈ ⋃ A ∪ B ↔ ∃ y x ∈ y ∧ y ∈ A ∪ B
12 elun ⊢ x ∈ ⋃ A ∪ ⋃ B ↔ x ∈ ⋃ A ∨ x ∈ ⋃ B
13 10 11 12 3bitr4i ⊢ x ∈ ⋃ A ∪ B ↔ x ∈ ⋃ A ∪ ⋃ B
14 13 eqriv ⊢ ⋃ A ∪ B = ⋃ A ∪ ⋃ B