This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfsymdif2

Description: Alternate definition of the symmetric difference. (Contributed by BJ, 30-Apr-2020)

		Ref	Expression
	Assertion	dfsymdif2	$⊢ (A ∆ B) = \{x \| (x \in A ⊻ x \in B)\}$

Step	Hyp	Ref	Expression
1		elsymdifxor	$⊢ x \in (A ∆ B) \leftrightarrow (x \in A ⊻ x \in B)$
2	1	eqabi	$⊢ (A ∆ B) = \{x \| (x \in A ⊻ x \in B)\}$