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 4286 | . . 3 ⊢ ∅ ⊆ 𝐴 | |
2 | eqss 3893 | . . 3 ⊢ (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴)) | |
3 | 1, 2 | mpbiran2 710 | . 2 ⊢ (𝐴 = ∅ ↔ 𝐴 ⊆ ∅) |
4 | 3 | bicomi 227 | 1 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1542 ⊆ wss 3844 ∅c0 4212 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-v 3401 df-dif 3847 df-in 3851 df-ss 3861 df-nul 4213 |
This theorem is referenced by: ss0 4288 un00 4333 pw0 4701 al0ssb 5177 fnsuppeq0 7890 cnfcom2lem 9240 card0 9463 kmlem5 9657 cf0 9754 fin1a2lem12 9914 mreexexlem3d 17023 efgval 18964 ppttop 21761 0nnei 21866 disjunsn 30510 isarchi 31016 filnetlem4 34216 bj-pw0ALT 34868 coss0 36243 pnonsingN 37593 osumcllem4N 37619 resnonrel 40768 ntrneicls11 41269 ntrneikb 41273 sprsymrelfvlem 44506 |
Copyright terms: Public domain | W3C validator |