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

Theorem ss0 3486
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 3485 . 2  |-  ( A 
C_  (/)  <->  A  =  (/) )
21biimpi 186 1  |-  ( A 
C_  (/)  ->  A  =  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    C_ wss 3153   (/)c0 3456
This theorem is referenced by:  sseq0  3487  abf  3489  eq0rdv  3490  ssdisj  3505  disjpss  3506  0dif  3526  dfopif  3794  fr0  4371  tfindsg  4650  findsg  4682  poirr2  5066  sofld  5120  f00  5392  frxp  6187  map0b  6802  sbthlem7  6973  phplem2  7037  fi0  7169  cantnflem1  7387  rankeq0b  7528  grur1a  8437  ixxdisj  10667  icodisj  10757  ioodisj  10761  uzdisj  10852  hashf1lem2  11390  sumz  12191  sumss  12193  fsum2dlem  12229  symgbas  14768  cntzval  14793  oppglsm  14949  efgval  15022  islss  15688  00lss  15695  mplsubglem  16175  ntrcls0  16809  neindisj2  16856  hauscmplem  17129  fbdmn0  17525  fbncp  17530  opnfbas  17533  fbasfip  17559  fbunfip  17560  fgcl  17569  supfil  17586  ufinffr  17620  alexsubALTlem2  17738  metnrmlem3  18361  itg1addlem4  19050  mdeg0  19452  uc1pval  19521  mon1pval  19523  pserulm  19794  derangsn  23108  vdgrun  23300  hdrmp  25117  coeq0i  26243  eldioph2lem2  26251  eldioph4b  26305  pcl0N  29390  pcl0bN  29391
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-dif 3156  df-in 3160  df-ss 3167  df-nul 3457
  Copyright terms: Public domain W3C validator