![]() |
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 4305 | . 2 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) | |
2 | 1 | biimpi 219 | 1 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = 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: sseq0 4307 0dif 4309 eq0rdv 4312 ssdisj 4367 disjpss 4368 dfopif 4760 iunxdif3 4980 fr0 5498 poirr2 5951 sofld 6011 f00 6535 tfindsg 7555 findsg 7590 frxp 7803 map0b 8430 sbthlem7 8617 phplem2 8681 fi0 8868 cantnflem1 9136 rankeq0b 9273 grur1a 10230 ixxdisj 12741 icodisj 12854 ioodisj 12860 uzdisj 12975 nn0disj 13018 hashf1lem2 13810 swrd0 14011 xptrrel 14331 sumz 15071 sumss 15073 fsum2dlem 15117 prod1 15290 prodss 15293 fprodss 15294 fprod2dlem 15326 cntzval 18443 oppglsm 18759 efgval 18835 islss 19699 00lss 19706 mplsubglem 20672 ntrcls0 21681 neindisj2 21728 hauscmplem 22011 fbdmn0 22439 fbncp 22444 opnfbas 22447 fbasfip 22473 fbunfip 22474 fgcl 22483 supfil 22500 ufinffr 22534 alexsubALTlem2 22653 metnrmlem3 23466 itg1addlem4 24303 uc1pval 24740 mon1pval 24742 pserulm 25017 vtxdun 27271 vtxdginducedm1 27333 difres 30363 imadifxp 30364 swrdrndisj 30657 cycpmco2f1 30816 esumrnmpt2 31437 truae 31612 carsgclctunlem2 31687 acycgr0v 32508 prclisacycgr 32511 derangsn 32530 poimirlem3 35060 ismblfin 35098 pcl0N 37218 pcl0bN 37219 coeq0i 39694 eldioph2lem2 39702 eldioph4b 39752 ntrk2imkb 40740 ntrk0kbimka 40742 ssin0 41689 iccdifprioo 42153 sumnnodd 42272 sge0split 43048 0setrec 45233 |
Copyright terms: Public domain | W3C validator |