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	$$⊢\left(A∆B\right)=\left(A\cup B\right)\setminus \left(A\cap B\right)$$

Proof

Step	Hyp	Ref	Expression
1		difin	$$⊢A\setminus \left(A\cap B\right)=A\setminus B$$
2		incom	$$⊢A\cap B=B\cap A$$
3	2	difeq2i	$$⊢B\setminus \left(A\cap B\right)=B\setminus \left(B\cap A\right)$$
4		difin	$$⊢B\setminus \left(B\cap A\right)=B\setminus A$$
5	3 4	eqtri	$$⊢B\setminus \left(A\cap B\right)=B\setminus A$$
6	1 5	uneq12i	$$⊢\left(A\setminus \left(A\cap B\right)\right)\cup \left(B\setminus \left(A\cap B\right)\right)=\left(A\setminus B\right)\cup \left(B\setminus A\right)$$
7		difundir	$$⊢\left(A\cup B\right)\setminus \left(A\cap B\right)=\left(A\setminus \left(A\cap B\right)\right)\cup \left(B\setminus \left(A\cap B\right)\right)$$
8		df-symdif	$$⊢\left(A∆B\right)=\left(A\setminus B\right)\cup \left(B\setminus A\right)$$
9	6 7 8	3eqtr4ri	$$⊢\left(A∆B\right)=\left(A\cup B\right)\setminus \left(A\cap B\right)$$