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

Theorem ss0 3498
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  |-  ( A 
C_  (/)  ->  A  =  (/) )

Proof of Theorem ss0
StepHypRef Expression
1 ss0b 3497 . 2  |-  ( A 
C_  (/)  <->  A  =  (/) )
21biimpi 186 1  |-  ( A 
C_  (/)  ->  A  =  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    C_ wss 3165   (/)c0 3468
This theorem is referenced by:  sseq0  3499  abf  3501  eq0rdv  3502  ssdisj  3517  disjpss  3518  0dif  3538  dfopif  3809  fr0  4388  tfindsg  4667  findsg  4699  poirr2  5083  sofld  5137  f00  5442  frxp  6241  map0b  6822  sbthlem7  6993  phplem2  7057  fi0  7189  cantnflem1  7407  rankeq0b  7548  grur1a  8457  ixxdisj  10687  icodisj  10777  ioodisj  10781  uzdisj  10872  hashf1lem2  11410  sumz  12211  sumss  12213  fsum2dlem  12249  symgbas  14788  cntzval  14813  oppglsm  14969  efgval  15042  islss  15708  00lss  15715  mplsubglem  16195  ntrcls0  16829  neindisj2  16876  hauscmplem  17149  fbdmn0  17545  fbncp  17550  opnfbas  17553  fbasfip  17579  fbunfip  17580  fgcl  17589  supfil  17606  ufinffr  17640  alexsubALTlem2  17758  metnrmlem3  18381  itg1addlem4  19070  mdeg0  19472  uc1pval  19541  mon1pval  19543  pserulm  19814  derangsn  23716  vdgrun  23908  prod1  24169  hdrmp  25809  coeq0i  26935  eldioph2lem2  26943  eldioph4b  26997  pcl0N  30733  pcl0bN  30734
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168  df-in 3172  df-ss 3179  df-nul 3469
  Copyright terms: Public domain W3C validator