Theorem 0dif

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

	Ref	Expression
Assertion	0dif	$$⊢\varnothing \setminus A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		difss	$$⊢\varnothing \setminus A\subseteq \varnothing$$
2		ss0	$$⊢\varnothing \setminus A\subseteq \varnothing \to \varnothing \setminus A=\varnothing$$
3	1 2	ax-mp	$$⊢\varnothing \setminus A=\varnothing$$