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

Proof

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