Theorem dfsymdif4

Description: Alternate definition of the symmetric difference. (Contributed by NM, 17-Aug-2004) (Revised by AV, 17-Aug-2022)

	Ref	Expression
Assertion	dfsymdif4	$$⊢\left(A∆B\right)=\left\{x|\neg \left(x\in A\leftrightarrow x\in B\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		elsymdif	$$⊢x\in \left(A∆B\right)\leftrightarrow \neg \left(x\in A\leftrightarrow x\in B\right)$$
2	1	eqabi	$$⊢\left(A∆B\right)=\left\{x|\neg \left(x\in A\leftrightarrow x\in B\right)\right\}$$