Metamath Proof Explorer

Theorem elsymdifxor

Description: Membership in a symmetric difference is an exclusive-or relationship. (Contributed by David A. Wheeler, 26-Apr-2020) (Proof shortened by BJ, 13-Aug-2022)

		Ref	Expression
	Assertion	elsymdifxor	$⊢ A \in (B ∆ C) \leftrightarrow (A \in B ⊻ A \in C)$

Proof

Step	Hyp	Ref	Expression
1		elsymdif	$⊢ A \in (B ∆ C) \leftrightarrow \neg (A \in B \leftrightarrow A \in C)$
2		df-xor	$⊢ (A \in B ⊻ A \in C) \leftrightarrow \neg (A \in B \leftrightarrow A \in C)$
3	1 2	bitr4i	$⊢ A \in (B ∆ C) \leftrightarrow (A \in B ⊻ A \in C)$