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 ⊢∃yx∈y∧y∈A∨x∈y∧y∈B↔∃yx∈y∧y∈A∨∃yx∈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 ⊢∃yx∈y∧y∈A∪B↔∃yx∈y∧y∈A∨x∈y∧y∈B
7 eluni ⊢x∈⋃A↔∃yx∈y∧y∈A
8 eluni ⊢x∈⋃B↔∃yx∈y∧y∈B
9 7 8 orbi12i ⊢x∈⋃A∨x∈⋃B↔∃yx∈y∧y∈A∨∃yx∈y∧y∈B
10 1 6 9 3bitr4i ⊢∃yx∈y∧y∈A∪B↔x∈⋃A∨x∈⋃B
11 eluni ⊢x∈⋃A∪B↔∃yx∈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