Theorem uneq2d

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

	Ref	Expression
Hypothesis	uneq1d.1	$$⊢\phi \to A=B$$
Assertion	uneq2d	$$⊢\phi \to C\cup A=C\cup B$$

Proof

Step	Hyp	Ref	Expression
1		uneq1d.1	$$⊢\phi \to A=B$$
2		uneq2	$$⊢A=B\to C\cup A=C\cup B$$
3	1 2	syl	$$⊢\phi \to C\cup A=C\cup B$$