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 3925 | . 2 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) | |
2 | 1 | biimpi 205 | 1 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ⊆ wss 3540 ∅c0 3874 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-dif 3543 df-in 3547 df-ss 3554 df-nul 3875 |
This theorem is referenced by: sseq0 3927 0dif 3929 eq0rdv 3931 ssdisj 3978 ssdisjOLD 3979 disjpss 3980 dfopif 4337 iunxdif3 4542 fr0 5017 poirr2 5439 sofld 5500 f00 6000 tfindsg 6952 findsg 6985 frxp 7174 map0b 7782 sbthlem7 7961 phplem2 8025 fi0 8209 cantnflem1 8469 rankeq0b 8606 grur1a 9520 ixxdisj 12061 icodisj 12168 ioodisj 12173 uzdisj 12282 nn0disj 12324 hashf1lem2 13097 swrd0 13286 xptrrel 13567 sumz 14300 sumss 14302 fsum2dlem 14343 prod1 14513 prodss 14516 fprodss 14517 fprod2dlem 14549 cntzval 17577 symgbas 17623 oppglsm 17880 efgval 17953 islss 18756 00lss 18763 mplsubglem 19255 ntrcls0 20690 neindisj2 20737 hauscmplem 21019 fbdmn0 21448 fbncp 21453 opnfbas 21456 fbasfip 21482 fbunfip 21483 fgcl 21492 supfil 21509 ufinffr 21543 alexsubALTlem2 21662 metnrmlem3 22472 itg1addlem4 23272 uc1pval 23703 mon1pval 23705 pserulm 23980 vdgrun 26428 vdgrfiun 26429 difres 28795 imadifxp 28796 esumrnmpt2 29457 truae 29633 carsgclctunlem2 29708 derangsn 30406 poimirlem3 32582 ismblfin 32620 pcl0N 34226 pcl0bN 34227 coeq0i 36334 eldioph2lem2 36342 eldioph4b 36393 ntrk2imkb 37355 ntrk0kbimka 37357 ssin0 38248 iccdifprioo 38589 sumnnodd 38697 sge0split 39302 vtxdun 40696 0setrec 42246 |
Copyright terms: Public domain | W3C validator |