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 abbi2i A B = x | x A x B