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	$$⊢\left(A∆\varnothing \right)=A$$

Proof

Step	Hyp	Ref	Expression
1		df-symdif	$$⊢\left(A∆\varnothing \right)=\left(A\setminus \varnothing \right)\cup \left(\varnothing \setminus A\right)$$
2		dif0	$$⊢A\setminus \varnothing =A$$
3		0dif	$$⊢\varnothing \setminus A=\varnothing$$
4	2 3	uneq12i	$$⊢\left(A\setminus \varnothing \right)\cup \left(\varnothing \setminus A\right)=A\cup \varnothing$$
5		un0	$$⊢A\cup \varnothing =A$$
6	1 4 5	3eqtri	$$⊢\left(A∆\varnothing \right)=A$$