![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ss0b | Structured version Visualization version GIF version |
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 |
---|---|
ss0b | ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0ss 4394 | . . 3 ⊢ ∅ ⊆ 𝐴 | |
2 | eqss 3994 | . . 3 ⊢ (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴)) | |
3 | 1, 2 | mpbiran2 708 | . 2 ⊢ (𝐴 = ∅ ↔ 𝐴 ⊆ ∅) |
4 | 3 | bicomi 223 | 1 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1534 ⊆ wss 3946 ∅c0 4322 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-dif 3949 df-ss 3963 df-nul 4323 |
This theorem is referenced by: ss0 4396 un00 4439 pw0 4811 al0ssb 5305 fnsuppeq0 8198 cnfcom2lem 9737 card0 9994 kmlem5 10190 cf0 10285 fin1a2lem12 10445 mreexexlem3d 17654 efgval 19711 ppttop 22998 0nnei 23104 disjunsn 32514 isarchi 33051 filnetlem4 36106 bj-pw0ALT 36769 coss0 38190 pnonsingN 39645 osumcllem4N 39671 resnonrel 43296 ntrneicls11 43794 ntrneikb 43798 sprsymrelfvlem 47098 isubgr0uhgr 47474 |
Copyright terms: Public domain | W3C validator |