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

Theorem ss0 3485
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 3484 . 2  |-  ( A 
C_  (/)  <->  A  =  (/) )
21biimpi 186 1  |-  ( A 
C_  (/)  ->  A  =  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    C_ wss 3152   (/)c0 3455
This theorem is referenced by:  sseq0  3486  abf  3488  eq0rdv  3489  ssdisj  3504  disjpss  3505  0dif  3525  dfopif  3793  fr0  4372  tfindsg  4651  findsg  4683  poirr2  5067  sofld  5121  f00  5426  frxp  6225  map0b  6806  sbthlem7  6977  phplem2  7041  fi0  7173  cantnflem1  7391  rankeq0b  7532  grur1a  8441  ixxdisj  10671  icodisj  10761  ioodisj  10765  uzdisj  10856  hashf1lem2  11394  sumz  12195  sumss  12197  fsum2dlem  12233  symgbas  14772  cntzval  14797  oppglsm  14953  efgval  15026  islss  15692  00lss  15699  mplsubglem  16179  ntrcls0  16813  neindisj2  16860  hauscmplem  17133  fbdmn0  17529  fbncp  17534  opnfbas  17537  fbasfip  17563  fbunfip  17564  fgcl  17573  supfil  17590  ufinffr  17624  alexsubALTlem2  17742  metnrmlem3  18365  itg1addlem4  19054  mdeg0  19456  uc1pval  19525  mon1pval  19527  pserulm  19798  derangsn  23701  vdgrun  23893  hdrmp  25706  coeq0i  26832  eldioph2lem2  26840  eldioph4b  26894  pcl0N  30111  pcl0bN  30112
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 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
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 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-in 3159  df-ss 3166  df-nul 3456
  Copyright terms: Public domain W3C validator