Definition df-symdif

Description: Define the symmetric difference of two classes. Alternate definitions are dfsymdif2 , dfsymdif3 and dfsymdif4 . (Contributed by Scott Fenton, 31-Mar-2012)

	Ref	Expression
Assertion	df-symdif	$$⊢\left(A∆B\right)=\left(A\setminus B\right)\cup \left(B\setminus A\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	csymdif	$$class\left(A∆B\right)$$
3	0 1	cdif	$$class\left(A\setminus B\right)$$
4	1 0	cdif	$$class\left(B\setminus A\right)$$
5	3 4	cun	$$class\left(\left(A\setminus B\right)\cup \left(B\setminus A\right)\right)$$
6	2 5	wceq	$$wff\left(A∆B\right)=\left(A\setminus B\right)\cup \left(B\setminus A\right)$$