Metamath Proof Explorer


Theorem npss0

Description: No set is a proper subset of the empty set. (Contributed by NM, 17-Jun-1998) (Proof shortened by Andrew Salmon, 26-Jun-2011) (Proof shortened by JJ, 14-Jul-2021)

Ref Expression
Assertion npss0 ¬ A

Proof

Step Hyp Ref Expression
1 0ss A
2 ssnpss A ¬ A
3 1 2 ax-mp ¬ A