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	⊢ ( 𝐴 △ 𝐵 ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	csymdif	⊢ ( 𝐴 △ 𝐵 )
3	0 1	cdif	⊢ ( 𝐴 ∖ 𝐵 )
4	1 0	cdif	⊢ ( 𝐵 ∖ 𝐴 )
5	3 4	cun	⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) )
6	2 5	wceq	⊢ ( 𝐴 △ 𝐵 ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) )