![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ss0 | Structured version Visualization version Unicode 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 3775 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpi 199 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-v 3058 df-dif 3418 df-in 3422 df-ss 3429 df-nul 3743 |
This theorem is referenced by: sseq0 3777 abf 3779 eq0rdv 3780 ssdisj 3825 disjpss 3826 0dif 3849 dfopif 4176 fr0 4831 poirr2 5242 sofld 5302 f00 5787 tfindsg 6713 findsg 6746 frxp 6932 map0b 7535 sbthlem7 7713 phplem2 7777 fi0 7959 cantnflem1 8219 rankeq0b 8356 grur1a 9269 ixxdisj 11678 icodisj 11785 ioodisj 11790 uzdisj 11895 nn0disj 11936 hashf1lem2 12651 swrd0 12826 xptrrel 13092 sumz 13836 sumss 13838 fsum2dlem 13879 prod1 14046 prodss 14049 fprodss 14050 fprod2dlem 14082 cntzval 17023 symgbas 17069 oppglsm 17342 efgval 17415 islss 18206 00lss 18213 mplsubglem 18706 ntrcls0 20140 neindisj2 20187 hauscmplem 20469 fbdmn0 20897 fbncp 20902 opnfbas 20905 fbasfip 20931 fbunfip 20932 fgcl 20941 supfil 20958 ufinffr 20992 alexsubALTlem2 21111 metnrmlem3 21926 metnrmlem3OLD 21941 itg1addlem4 22705 uc1pval 23138 mon1pval 23140 pserulm 23425 vdgrun 25677 vdgrfiun 25678 iunxdif3 28223 difres 28259 imadifxp 28260 esumrnmpt2 28937 truae 29114 carsgclctunlem2 29199 derangsn 29941 poimirlem3 31987 ismblfin 32025 pcl0N 33531 pcl0bN 33532 coeq0i 35639 eldioph2lem2 35647 eldioph4b 35698 ssin0 37432 iccdifprioo 37654 sumnnodd 37747 sge0split 38288 vtxduhgrun 39587 |
Copyright terms: Public domain | W3C validator |