Theorem uneq2

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

	Ref	Expression
Assertion	uneq2	$$⊢A=B\to C\cup A=C\cup B$$

Proof

Step	Hyp	Ref	Expression
1		uneq1	$$⊢A=B\to A\cup C=B\cup C$$
2		uncom	$$⊢C\cup A=A\cup C$$
3		uncom	$$⊢C\cup B=B\cup C$$
4	1 2 3	3eqtr4g	$$⊢A=B\to C\cup A=C\cup B$$