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

Metamath Proof Explorer

Theorem uneq2d

Description: Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998)

Ref Expression
Hypothesis uneq1d.1 ⊢ φ → A = B
Assertion uneq2d ⊢ φ → C ∪ A = C ∪ B

Proof

Step Hyp Ref Expression
1 uneq1d.1 ⊢ φ → A = B
2 uneq2 ⊢ A = B → C ∪ A = C ∪ B
3 1 2 syl ⊢ φ → C ∪ A = C ∪ B