Theorem symdifeq1

Description: Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012)

	Ref	Expression
Assertion	symdifeq1	$$⊢A=B\to \left(A∆C\right)=\left(B∆C\right)$$

Proof

Step	Hyp	Ref	Expression
1		difeq1	$$⊢A=B\to A\setminus C=B\setminus C$$
2		difeq2	$$⊢A=B\to C\setminus A=C\setminus B$$
3	1 2	uneq12d	$$⊢A=B\to \left(A\setminus C\right)\cup \left(C\setminus A\right)=\left(B\setminus C\right)\cup \left(C\setminus B\right)$$
4		df-symdif	$$⊢\left(A∆C\right)=\left(A\setminus C\right)\cup \left(C\setminus A\right)$$
5		df-symdif	$$⊢\left(B∆C\right)=\left(B\setminus C\right)\cup \left(C\setminus B\right)$$
6	3 4 5	3eqtr4g	$$⊢A=B\to \left(A∆C\right)=\left(B∆C\right)$$