![]() |
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 4168 | . . 3 ⊢ ∅ ⊆ 𝐴 | |
2 | eqss 3813 | . . 3 ⊢ (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴)) | |
3 | 1, 2 | mpbiran2 702 | . 2 ⊢ (𝐴 = ∅ ↔ 𝐴 ⊆ ∅) |
4 | 3 | bicomi 216 | 1 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 = wceq 1653 ⊆ wss 3769 ∅c0 4115 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-v 3387 df-dif 3772 df-in 3776 df-ss 3783 df-nul 4116 |
This theorem is referenced by: ss0 4170 un00 4207 pw0 4531 al0ssb 4985 fnsuppeq0 7561 cnfcom2lem 8848 card0 9070 kmlem5 9264 cf0 9361 fin1a2lem12 9521 mreexexlem3d 16621 efgval 18443 ppttop 21140 0nnei 21245 disjunsn 29924 isarchi 30252 filnetlem4 32888 coss0 34723 pnonsingN 35954 osumcllem4N 35980 resnonrel 38681 ntrneicls11 39170 ntrneikb 39174 sprsymrelfvlem 42539 |
Copyright terms: Public domain | W3C validator |