| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ss0 | Structured version Visualization version GIF version | ||
| Description: Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23. (Contributed by NM, 13-Aug-1994.) |
| Ref | Expression |
|---|---|
| ss0 | ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ss0b 4401 | . 2 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) | |
| 2 | 1 | biimpi 216 | 1 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = 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: sseq0 4403 0dif 4405 eq0rdvALT 4408 ssdisj 4460 disjpss 4461 dfopif 4870 iunxdif3 5095 fr0 5663 poirr2 6144 sofld 6207 f00 6790 fvmptopab 7487 tfindsg 7882 findsg 7919 frxp 8151 map0b 8923 sbthlem7 9129 ssfi 9213 phplem2OLD 9255 fi0 9460 cantnflem1 9729 rankeq0b 9900 grur1a 10859 ixxdisj 13402 icodisj 13516 ioodisj 13522 uzdisj 13637 nn0disj 13684 hashf1lem2 14495 swrd0 14696 xptrrel 15019 sumz 15758 sumss 15760 fsum2dlem 15806 prod1 15980 prodss 15983 fprodss 15984 fprod2dlem 16016 cntzval 19339 oppglsm 19660 efgval 19735 islss 20932 00lss 20939 mplsubglem 22019 ntrcls0 23084 neindisj2 23131 hauscmplem 23414 fbdmn0 23842 fbncp 23847 opnfbas 23850 fbasfip 23876 fbunfip 23877 fgcl 23886 supfil 23903 ufinffr 23937 alexsubALTlem2 24056 metnrmlem3 24883 itg1addlem4 25734 uc1pval 26179 mon1pval 26181 pserulm 26465 vtxdun 29499 vtxdginducedm1 29561 difres 32613 imadifxp 32614 swrdrndisj 32942 cycpmco2f1 33144 erlval 33262 ssdifidllem 33484 ply1dg3rt0irred 33607 esumrnmpt2 34069 truae 34244 carsgclctunlem2 34321 acycgr0v 35153 prclisacycgr 35156 derangsn 35175 poimirlem3 37630 ismblfin 37668 pcl0N 39924 pcl0bN 39925 coeq0i 42764 eldioph2lem2 42772 eldioph4b 42822 oe0suclim 43290 ntrk2imkb 44050 ntrk0kbimka 44052 ssin0 45060 iccdifprioo 45529 sumnnodd 45645 sge0split 46424 iscnrm3llem2 48847 0setrec 49223 |
| Copyright terms: Public domain | W3C validator |