Theorem dfsymdif3

Description: Alternate definition of the symmetric difference, given in Example 4.1 of Stoll p. 262 (the original definition corresponds to Stoll p. 13). (Contributed by NM, 17-Aug-2004) (Revised by BJ, 30-Apr-2020)

	Ref	Expression
Assertion	dfsymdif3	⊢ ( 𝐴 △ 𝐵 ) = ( ( 𝐴 ∪ 𝐵 ) ∖ ( 𝐴 ∩ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		difin	⊢ ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 )
2		incom	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
3	2	difeq2i	⊢ ( 𝐵 ∖ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐵 ∖ ( 𝐵 ∩ 𝐴 ) )
4		difin	⊢ ( 𝐵 ∖ ( 𝐵 ∩ 𝐴 ) ) = ( 𝐵 ∖ 𝐴 )
5	3 4	eqtri	⊢ ( 𝐵 ∖ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐵 ∖ 𝐴 )
6	1 5	uneq12i	⊢ ( ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐵 ∖ ( 𝐴 ∩ 𝐵 ) ) ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) )
7		difundir	⊢ ( ( 𝐴 ∪ 𝐵 ) ∖ ( 𝐴 ∩ 𝐵 ) ) = ( ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐵 ∖ ( 𝐴 ∩ 𝐵 ) ) )
8		df-symdif	⊢ ( 𝐴 △ 𝐵 ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) )
9	6 7 8	3eqtr4ri	⊢ ( 𝐴 △ 𝐵 ) = ( ( 𝐴 ∪ 𝐵 ) ∖ ( 𝐴 ∩ 𝐵 ) )