Theorem symdif0

Description: Symmetric difference with the empty class. The empty class is the identity element for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012)

	Ref	Expression
Assertion	symdif0	⊢ ( 𝐴 △ ∅ ) = 𝐴

Proof

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