Metamath Proof Explorer


Theorem dfsymdif2

Description: Alternate definition of the symmetric difference. (Contributed by BJ, 30-Apr-2020)

Ref Expression
Assertion dfsymdif2 AB=x|xAxB

Proof

Step Hyp Ref Expression
1 elsymdifxor xABxAxB
2 1 abbi2i AB=x|xAxB