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	|- ( A /_\ B ) = ( ( A \ B ) u. ( B \ A ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2	0 1	csymdif	|- ( A /_\ B )
3	0 1	cdif	|- ( A \ B )
4	1 0	cdif	|- ( B \ A )
5	3 4	cun	|- ( ( A \ B ) u. ( B \ A ) )
6	2 5	wceq	|- ( A /_\ B ) = ( ( A \ B ) u. ( B \ A ) )