![]() |
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 4108 | . 2 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) | |
2 | 1 | biimpi 206 | 1 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1624 ⊆ wss 3707 ∅c0 4050 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-v 3334 df-dif 3710 df-in 3714 df-ss 3721 df-nul 4051 |
This theorem is referenced by: sseq0 4110 0dif 4112 eq0rdv 4114 ssdisj 4162 ssdisjOLD 4163 disjpss 4164 dfopif 4542 iunxdif3 4750 fr0 5237 poirr2 5670 sofld 5731 f00 6240 tfindsg 7217 findsg 7250 frxp 7447 map0b 8054 sbthlem7 8233 phplem2 8297 fi0 8483 cantnflem1 8751 rankeq0b 8888 grur1a 9825 ixxdisj 12375 icodisj 12482 ioodisj 12487 uzdisj 12598 nn0disj 12641 hashf1lem2 13424 swrd0 13626 xptrrel 13912 sumz 14644 sumss 14646 fsum2dlem 14692 prod1 14865 prodss 14868 fprodss 14869 fprod2dlem 14901 cntzval 17946 symgbas 17992 oppglsm 18249 efgval 18322 islss 19129 00lss 19136 mplsubglem 19628 ntrcls0 21074 neindisj2 21121 hauscmplem 21403 fbdmn0 21831 fbncp 21836 opnfbas 21839 fbasfip 21865 fbunfip 21866 fgcl 21875 supfil 21892 ufinffr 21926 alexsubALTlem2 22045 metnrmlem3 22857 itg1addlem4 23657 uc1pval 24090 mon1pval 24092 pserulm 24367 vtxdun 26579 vtxdginducedm1 26641 difres 29712 imadifxp 29713 esumrnmpt2 30431 truae 30607 carsgclctunlem2 30682 derangsn 31451 poimirlem3 33717 ismblfin 33755 pcl0N 35703 pcl0bN 35704 coeq0i 37810 eldioph2lem2 37818 eldioph4b 37869 ntrk2imkb 38829 ntrk0kbimka 38831 ssin0 39714 iccdifprioo 40237 sumnnodd 40357 sge0split 41121 0setrec 42952 |
Copyright terms: Public domain | W3C validator |