This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊆ ∅ ↔ A = ∅

Proof

Step Hyp Ref Expression
1 0ss ⊢ ∅ ⊆ A
2 eqss ⊢ A = ∅ ↔ A ⊆ ∅ ∧ ∅ ⊆ A
3 1 2 mpbiran2 ⊢ A = ∅ ↔ A ⊆ ∅
4 3 bicomi ⊢ A ⊆ ∅ ↔ A = ∅