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	⊢ ( ∅ ∖ 𝐴 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		difss	⊢ ( ∅ ∖ 𝐴 ) ⊆ ∅
2		ss0	⊢ ( ( ∅ ∖ 𝐴 ) ⊆ ∅ → ( ∅ ∖ 𝐴 ) = ∅ )
3	1 2	ax-mp	⊢ ( ∅ ∖ 𝐴 ) = ∅