Metamath Proof Explorer

Theorem ss0b

Description: Any subset of the empty set is empty. Theorem 5 of Suppes p. 23 and its converse. (Contributed by NM, 17-Sep-2003)

Ref Expression
Assertion ss0b 
|- ( A C_ (/) <-> A = (/) )

Proof

Step Hyp Ref Expression
1 0ss 
 |-  (/) C_ A
2 eqss 
 |-  ( A = (/) <-> ( A C_ (/) /\ (/) C_ A ) )
3 1 2 mpbiran2 
 |-  ( A = (/) <-> A C_ (/) )
4 3 bicomi 
 |-  ( A C_ (/) <-> A = (/) )