Metamath Proof Explorer

Theorem symdifid

Description: The symmetric difference of a class with itself is the empty class. (Contributed by Scott Fenton, 25-Apr-2012)

Ref Expression
Assertion symdifid 
|- ( A /_\ A ) = (/)

Proof

Step Hyp Ref Expression
1 df-symdif 
 |-  ( A /_\ A ) = ( ( A \ A ) u. ( A \ A ) )
2 difid 
 |-  ( A \ A ) = (/)
3 2 2 uneq12i 
 |-  ( ( A \ A ) u. ( A \ A ) ) = ( (/) u. (/) )
4 un0 
 |-  ( (/) u. (/) ) = (/)
5 1 3 4 3eqtri 
 |-  ( A /_\ A ) = (/)