Metamath Proof Explorer

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 
|- ( (/) \ A ) = (/)

Proof

Step Hyp Ref Expression
1 difss 
 |-  ( (/) \ A ) C_ (/)
2 ss0 
 |-  ( ( (/) \ A ) C_ (/) -> ( (/) \ A ) = (/) )
3 1 2 ax-mp 
 |-  ( (/) \ A ) = (/)