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 ⊢ A ∆ A = ∅

Proof

Step Hyp Ref Expression
1 df-symdif ⊢ A ∆ A = A ∖ A ∪ A ∖ A
2 difid ⊢ A ∖ A = ∅
3 2 2 uneq12i ⊢ A ∖ A ∪ A ∖ A = ∅ ∪ ∅
4 un0 ⊢ ∅ ∪ ∅ = ∅
5 1 3 4 3eqtri ⊢ A ∆ A = ∅