Metamath Proof Explorer

Theorem 0pss

Description: The null set is a proper subset of any nonempty set. (Contributed by NM, 27-Feb-1996)

Ref Expression
Assertion 0pss A A


Step Hyp Ref Expression
1 0ss A
2 df-pss A A A
3 1 2 mpbiran A A
4 necom A A
5 3 4 bitri A A