Theorem uneq1

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

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

Proof

Step	Hyp	Ref	Expression
1		eleq2	$$⊢A=B\to \left(x\in A\leftrightarrow x\in B\right)$$
2	1	orbi1d	$$⊢A=B\to \left(\left(x\in A\vee x\in C\right)\leftrightarrow \left(x\in B\vee x\in C\right)\right)$$
3		elun	$$⊢x\in \left(A\cup C\right)\leftrightarrow \left(x\in A\vee x\in C\right)$$
4		elun	$$⊢x\in \left(B\cup C\right)\leftrightarrow \left(x\in B\vee x\in C\right)$$
5	2 3 4	3bitr4g	$$⊢A=B\to \left(x\in \left(A\cup C\right)\leftrightarrow x\in \left(B\cup C\right)\right)$$
6	5	eqrdv	$$⊢A=B\to A\cup C=B\cup C$$