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

Metamath Proof Explorer

Theorem uncom

Description: Commutative law for union of classes. Exercise 6 of TakeutiZaring p. 17. (Contributed by NM, 25-Jun-1998) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion uncom ⊢ A ∪ B = B ∪ A

Proof

Step Hyp Ref Expression
1 orcom ⊢ x ∈ A ∨ x ∈ B ↔ x ∈ B ∨ x ∈ A
2 elun ⊢ x ∈ B ∪ A ↔ x ∈ B ∨ x ∈ A
3 1 2 bitr4i ⊢ x ∈ A ∨ x ∈ B ↔ x ∈ B ∪ A
4 3 uneqri ⊢ A ∪ B = B ∪ A