![]() |
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 4304 | . . 3 ⊢ ∅ ⊆ 𝐴 | |
2 | eqss 3930 | . . 3 ⊢ (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴)) | |
3 | 1, 2 | mpbiran2 709 | . 2 ⊢ (𝐴 = ∅ ↔ 𝐴 ⊆ ∅) |
4 | 3 | bicomi 227 | 1 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1538 ⊆ wss 3881 ∅c0 4243 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-dif 3884 df-in 3888 df-ss 3898 df-nul 4244 |
This theorem is referenced by: ss0 4306 un00 4350 pw0 4705 al0ssb 5176 fnsuppeq0 7841 cnfcom2lem 9148 card0 9371 kmlem5 9565 cf0 9662 fin1a2lem12 9822 mreexexlem3d 16909 efgval 18835 ppttop 21612 0nnei 21717 disjunsn 30357 isarchi 30861 filnetlem4 33842 bj-pw0ALT 34466 coss0 35879 pnonsingN 37229 osumcllem4N 37255 resnonrel 40292 ntrneicls11 40793 ntrneikb 40797 sprsymrelfvlem 44007 |
Copyright terms: Public domain | W3C validator |