Metamath Proof Explorer

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

Proof

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