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

Proof

Step Hyp Ref Expression
1 0ss
 |-  (/) C_ A
2 df-pss
 |-  ( (/) C. A <-> ( (/) C_ A /\ (/) =/= A ) )
3 1 2 mpbiran
 |-  ( (/) C. A <-> (/) =/= A )
4 necom
 |-  ( (/) =/= A <-> A =/= (/) )
5 3 4 bitri
 |-  ( (/) C. A <-> A =/= (/) )