![]() |
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 4396 | . 2 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) | |
2 | 1 | biimpi 215 | 1 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ⊆ wss 3947 ∅c0 4321 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-dif 3950 df-in 3954 df-ss 3964 df-nul 4322 |
This theorem is referenced by: sseq0 4398 0dif 4400 eq0rdvALT 4404 ssdisj 4458 disjpss 4459 dfopif 4869 iunxdif3 5097 fr0 5654 poirr2 6122 sofld 6183 f00 6770 fvmptopab 7458 tfindsg 7845 findsg 7885 frxp 8107 map0b 8873 sbthlem7 9085 ssfi 9169 phplem2OLD 9214 fi0 9411 cantnflem1 9680 rankeq0b 9851 grur1a 10810 ixxdisj 13335 icodisj 13449 ioodisj 13455 uzdisj 13570 nn0disj 13613 hashf1lem2 14413 swrd0 14604 xptrrel 14923 sumz 15664 sumss 15666 fsum2dlem 15712 prod1 15884 prodss 15887 fprodss 15888 fprod2dlem 15920 cntzval 19179 oppglsm 19503 efgval 19578 islss 20533 00lss 20540 mplsubglem 21540 ntrcls0 22562 neindisj2 22609 hauscmplem 22892 fbdmn0 23320 fbncp 23325 opnfbas 23328 fbasfip 23354 fbunfip 23355 fgcl 23364 supfil 23381 ufinffr 23415 alexsubALTlem2 23534 metnrmlem3 24359 itg1addlem4 25198 itg1addlem4OLD 25199 uc1pval 25639 mon1pval 25641 pserulm 25916 vtxdun 28718 vtxdginducedm1 28780 difres 31809 imadifxp 31810 swrdrndisj 32099 cycpmco2f1 32261 esumrnmpt2 33004 truae 33179 carsgclctunlem2 33256 acycgr0v 34077 prclisacycgr 34080 derangsn 34099 poimirlem3 36429 ismblfin 36467 pcl0N 38731 pcl0bN 38732 coeq0i 41424 eldioph2lem2 41432 eldioph4b 41482 oe0suclim 41960 ntrk2imkb 42721 ntrk0kbimka 42723 ssin0 43675 iccdifprioo 44164 sumnnodd 44281 sge0split 45060 iscnrm3llem2 47485 0setrec 47651 |
Copyright terms: Public domain | W3C validator |