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