Theorem symdifcom

Description: Symmetric difference commutes. (Contributed by Scott Fenton, 24-Apr-2012)

	Ref	Expression
Assertion	symdifcom	$$⊢\left(A∆B\right)=\left(B∆A\right)$$

Proof

Step	Hyp	Ref	Expression
1		uncom	$$⊢\left(A\setminus B\right)\cup \left(B\setminus A\right)=\left(B\setminus A\right)\cup \left(A\setminus B\right)$$
2		df-symdif	$$⊢\left(A∆B\right)=\left(A\setminus B\right)\cup \left(B\setminus A\right)$$
3		df-symdif	$$⊢\left(B∆A\right)=\left(B\setminus A\right)\cup \left(A\setminus B\right)$$
4	1 2 3	3eqtr4i	$$⊢\left(A∆B\right)=\left(B∆A\right)$$