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 4296 | . 2 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) | |
2 | 1 | biimpi 219 | 1 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ⊆ wss 3853 ∅c0 4221 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-v 3402 df-dif 3856 df-in 3860 df-ss 3870 df-nul 4222 |
This theorem is referenced by: sseq0 4298 0dif 4300 eq0rdvALT 4304 ssdisj 4359 disjpss 4360 dfopifOLD 4766 iunxdif3 4990 fr0 5514 poirr2 5968 sofld 6029 f00 6571 tfindsg 7607 findsg 7643 frxp 7859 map0b 8506 sbthlem7 8696 phplem2 8760 ssfi 8785 fi0 8970 cantnflem1 9238 rankeq0b 9375 grur1a 10332 ixxdisj 12849 icodisj 12963 ioodisj 12969 uzdisj 13084 nn0disj 13127 hashf1lem2 13921 swrd0 14122 xptrrel 14442 sumz 15185 sumss 15187 fsum2dlem 15231 prod1 15403 prodss 15406 fprodss 15407 fprod2dlem 15439 cntzval 18582 oppglsm 18898 efgval 18974 islss 19838 00lss 19845 mplsubglem 20828 ntrcls0 21840 neindisj2 21887 hauscmplem 22170 fbdmn0 22598 fbncp 22603 opnfbas 22606 fbasfip 22632 fbunfip 22633 fgcl 22642 supfil 22659 ufinffr 22693 alexsubALTlem2 22812 metnrmlem3 23626 itg1addlem4 24464 itg1addlem4OLD 24465 uc1pval 24905 mon1pval 24907 pserulm 25182 vtxdun 27436 vtxdginducedm1 27498 difres 30526 imadifxp 30527 swrdrndisj 30817 cycpmco2f1 30981 esumrnmpt2 31619 truae 31794 carsgclctunlem2 31869 acycgr0v 32694 prclisacycgr 32697 derangsn 32716 poimirlem3 35436 ismblfin 35474 pcl0N 37592 pcl0bN 37593 coeq0i 40188 eldioph2lem2 40196 eldioph4b 40246 ntrk2imkb 41234 ntrk0kbimka 41236 ssin0 42182 iccdifprioo 42635 sumnnodd 42754 sge0split 43530 iscnrm3llem2 45814 0setrec 45910 |
Copyright terms: Public domain | W3C validator |