ss0 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ss0		Structured version Unicode version

Theorem ss0 3815

Description: Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23. (Contributed by NM, 13-Aug-1994.)

**Assertion**
Ref	Expression
ss0

**Proof of Theorem ss0**
Step	Hyp	Ref	Expression
1		ss0b 3814	. 2
2	1	biimpi 194	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1398

wss 3461

c0 3783

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432

This theorem depends on definitions: df-bi 185 df-an 369 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-v 3108 df-dif 3464 df-in 3468 df-ss 3475 df-nul 3784

This theorem is referenced by: sseq0 3816 abf 3818 eq0rdv 3819 ssdisj 3864 disjpss 3865 0dif 3887 dfopif 4200 fr0 4847 poirr2 5379 sofld 5439 f00 5749 tfindsg 6668 findsg 6700 frxp 6883 map0b 7450 sbthlem7 7626 phplem2 7690 fi0 7872 cantnflem1 8099 cantnflem1OLD 8122 rankeq0b 8269 grur1a 9186 ixxdisj 11547 icodisj 11648 ioodisj 11653 uzdisj 11755 nn0disj 11795 hashf1lem2 12492 swrd0 12653 xptrrel 12901 sumz 13629 sumss 13631 fsum2dlem 13670 prod1 13836 prodss 13839 fprodss 13840 fprod2dlem 13869 cntzval 16561 symgbas 16607 oppglsm 16864 efgval 16937 islss 17779 00lss 17786 mplsubglem 18291 mplsubglemOLD 18293 ntrcls0 19747 neindisj2 19794 hauscmplem 20076 fbdmn0 20504 fbncp 20509 opnfbas 20512 fbasfip 20538 fbunfip 20539 fgcl 20548 supfil 20565 ufinffr 20599 alexsubALTlem2 20717 metnrmlem3 21534 itg1addlem4 22275 uc1pval 22709 mon1pval 22711 pserulm 22986 vdgrun 25106 vdgrfiun 25107 iunxdif3 27640 difres 27674 imadifxp 27675 esumrnmpt2 28300 truae 28455 carsgclctunlem2 28530 derangsn 28881 ismblfin 30298 coeq0i 30928 eldioph2lem2 30936 eldioph4b 30987 iccdifprioo 31798 sumnnodd 31878 pcl0N 36062 pcl0bN 36063