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

Metamath Proof Explorer

Theorem uneq2

Description: Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993)

Ref Expression
Assertion uneq2 ⊢ A = B → C ∪ A = C ∪ B

Proof

Step Hyp Ref Expression
1 uneq1 ⊢ A = B → A ∪ C = B ∪ C
2 uncom ⊢ C ∪ A = A ∪ C
3 uncom ⊢ C ∪ B = B ∪ C
4 1 2 3 3eqtr4g ⊢ A = B → C ∪ A = C ∪ B