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 e. A \/_ x e. B ) }

Proof

Step Hyp Ref Expression
1 elsymdifxor 
 |-  ( x e. ( A /_\ B ) <-> ( x e. A \/_ x e. B ) )
2 1 eqabi 
 |-  ( A /_\ B ) = { x | ( x e. A \/_ x e. B ) }