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 ∈ A ⊻ x ∈ B

Proof

Step Hyp Ref Expression
1 elsymdifxor ⊢ x ∈ A ∆ B ↔ x ∈ A ⊻ x ∈ B
2 1 eqabi ⊢ A ∆ B = x | x ∈ A ⊻ x ∈ B