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

Theorem ss0 3816
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
StepHypRef Expression
1 ss0b 3815 . 2
21biimpi 194 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  C_wss 3475   c0 3784
This theorem is referenced by:  sseq0  3817  abf  3819  eq0rdv  3820  ssdisj  3876  disjpss  3877  0dif  3899  dfopif  4214  fr0  4863  poirr2  5396  sofld  5460  f00  5772  tfindsg  6695  findsg  6727  frxp  6910  map0b  7477  sbthlem7  7653  phplem2  7717  fi0  7900  cantnflem1  8129  cantnflem1OLD  8152  rankeq0b  8299  grur1a  9218  ixxdisj  11573  icodisj  11674  ioodisj  11679  uzdisj  11780  nn0disj  11820  hashf1lem2  12505  swrd0  12658  sumz  13544  sumss  13546  fsum2dlem  13585  prod1  13751  prodss  13754  fprodss  13755  fprod2dlem  13784  cntzval  16359  symgbas  16405  oppglsm  16662  efgval  16735  islss  17581  00lss  17588  mplsubglem  18093  mplsubglemOLD  18095  ntrcls0  19577  neindisj2  19624  hauscmplem  19906  fbdmn0  20335  fbncp  20340  opnfbas  20343  fbasfip  20369  fbunfip  20370  fgcl  20379  supfil  20396  ufinffr  20430  alexsubALTlem2  20548  metnrmlem3  21365  itg1addlem4  22106  uc1pval  22540  mon1pval  22542  pserulm  22817  vdgrun  24901  vdgrfiun  24902  difres  27457  imadifxp  27458  truae  28215  derangsn  28614  ismblfin  30055  coeq0i  30686  eldioph2lem2  30694  eldioph4b  30745  iccdifprioo  31556  sumnnodd  31636  pcl0N  35646  pcl0bN  35647  xptrrel  37775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489  df-nul 3785
  Copyright terms: Public domain W3C validator