This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 △ 𝐴 ) = ∅

Proof

Step Hyp Ref Expression
1 df-symdif ⊢ ( 𝐴 △ 𝐴 ) = ( ( 𝐴 ∖ 𝐴 ) ∪ ( 𝐴 ∖ 𝐴 ) )
2 difid ⊢ ( 𝐴 ∖ 𝐴 ) = ∅
3 2 2 uneq12i ⊢ ( ( 𝐴 ∖ 𝐴 ) ∪ ( 𝐴 ∖ 𝐴 ) ) = ( ∅ ∪ ∅ )
4 un0 ⊢ ( ∅ ∪ ∅ ) = ∅
5 1 3 4 3eqtri ⊢ ( 𝐴 △ 𝐴 ) = ∅