Theorem uneq12

Description: Equality theorem for the union of two classes. (Contributed by NM, 29-Mar-1998)

	Ref	Expression
Assertion	uneq12	$$⊢\left(A=B\wedge C=D\right)\to A\cup C=B\cup D$$

Proof

Step	Hyp	Ref	Expression
1		uneq1	$$⊢A=B\to A\cup C=B\cup C$$
2		uneq2	$$⊢C=D\to B\cup C=B\cup D$$
3	1 2	sylan9eq	$$⊢\left(A=B\wedge C=D\right)\to A\cup C=B\cup D$$