Theorem dif0

Description: The difference between a class and the empty set. Part of Exercise 4.4 of Stoll p. 16. (Contributed by NM, 17-Aug-2004)

	Ref	Expression
Assertion	dif0	$$⊢A\setminus \varnothing =A$$

Proof

Step	Hyp	Ref	Expression
1		difid	$$⊢A\setminus A=\varnothing$$
2	1	difeq2i	$$⊢A\setminus \left(A\setminus A\right)=A\setminus \varnothing$$
3		difdif	$$⊢A\setminus \left(A\setminus A\right)=A$$
4	2 3	eqtr3i	$$⊢A\setminus \varnothing =A$$