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 4350 | . 2 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) | |
2 | 1 | biimpi 218 | 1 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ⊆ wss 3935 ∅c0 4290 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-dif 3938 df-in 3942 df-ss 3951 df-nul 4291 |
This theorem is referenced by: sseq0 4352 0dif 4354 eq0rdv 4356 ssdisj 4408 disjpss 4409 dfopif 4799 iunxdif3 5016 fr0 5533 poirr2 5983 sofld 6043 f00 6560 tfindsg 7574 findsg 7608 frxp 7819 map0b 8446 sbthlem7 8632 phplem2 8696 fi0 8883 cantnflem1 9151 rankeq0b 9288 grur1a 10240 ixxdisj 12752 icodisj 12861 ioodisj 12867 uzdisj 12979 nn0disj 13022 hashf1lem2 13813 swrd0 14019 xptrrel 14339 sumz 15078 sumss 15080 fsum2dlem 15124 prod1 15297 prodss 15300 fprodss 15301 fprod2dlem 15333 cntzval 18450 oppglsm 18766 efgval 18842 islss 19705 00lss 19712 mplsubglem 20213 ntrcls0 21683 neindisj2 21730 hauscmplem 22013 fbdmn0 22441 fbncp 22446 opnfbas 22449 fbasfip 22475 fbunfip 22476 fgcl 22485 supfil 22502 ufinffr 22536 alexsubALTlem2 22655 metnrmlem3 23468 itg1addlem4 24299 uc1pval 24732 mon1pval 24734 pserulm 25009 vtxdun 27262 vtxdginducedm1 27324 difres 30349 imadifxp 30350 swrdrndisj 30631 cycpmco2f1 30766 esumrnmpt2 31327 truae 31502 carsgclctunlem2 31577 acycgr0v 32395 prclisacycgr 32398 derangsn 32417 poimirlem3 34894 ismblfin 34932 pcl0N 37057 pcl0bN 37058 coeq0i 39348 eldioph2lem2 39356 eldioph4b 39406 ntrk2imkb 40385 ntrk0kbimka 40387 ssin0 41315 iccdifprioo 41790 sumnnodd 41909 sge0split 42690 0setrec 44805 |
Copyright terms: Public domain | W3C validator |