Description: Any subset of the empty set is empty. Theorem 5 of Suppes p. 23. (Contributed by NM, 13-Aug-1994)
Ref | Expression | ||
---|---|---|---|
Assertion | ss0 | ⊢ ( 𝐴 ⊆ ∅ → 𝐴 = ∅ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ss0b | ⊢ ( 𝐴 ⊆ ∅ ↔ 𝐴 = ∅ ) | |
2 | 1 | biimpi | ⊢ ( 𝐴 ⊆ ∅ → 𝐴 = ∅ ) |