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