| 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 4400 | . . 3 ⊢ ∅ ⊆ 𝐴 | |
| 2 | eqss 3999 | . . 3 ⊢ (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴)) | |
| 3 | 1, 2 | mpbiran2 710 | . 2 ⊢ (𝐴 = ∅ ↔ 𝐴 ⊆ ∅) |
| 4 | 3 | bicomi 224 | 1 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 = wceq 1540 ⊆ wss 3951 ∅c0 4333 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-dif 3954 df-ss 3968 df-nul 4334 |
| This theorem is referenced by: ss0 4402 un00 4445 pw0 4812 al0ssb 5308 fnsuppeq0 8217 cnfcom2lem 9741 card0 9998 kmlem5 10195 cf0 10291 fin1a2lem12 10451 mreexexlem3d 17689 efgval 19735 ppttop 23014 0nnei 23120 disjunsn 32607 isarchi 33189 filnetlem4 36382 bj-pw0ALT 37050 coss0 38480 pnonsingN 39935 osumcllem4N 39961 resnonrel 43605 ntrneicls11 44103 ntrneikb 44107 sprsymrelfvlem 47477 isubgr0uhgr 47859 |
| Copyright terms: Public domain | W3C validator |