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

Theorem ss0 3427
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 3426 . 2  |-  ( A 
C_  (/)  <->  A  =  (/) )
21biimpi 188 1  |-  ( A 
C_  (/)  ->  A  =  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619    C_ wss 3094   (/)c0 3397
This theorem is referenced by:  sseq0  3428  abf  3430  eq0rdv  3431  ssdisj  3446  disjpss  3447  0dif  3467  dfopif  3734  fr0  4309  tfindsg  4588  findsg  4620  poirr2  5020  sofld  5074  f00  5329  frxp  6124  map0b  6739  sbthlem7  6910  phplem2  6974  fi0  7106  cantnflem1  7324  rankeq0b  7465  grur1a  8374  ixxdisj  10602  icodisj  10692  ioodisj  10696  uzdisj  10787  hashf1lem2  11324  sumz  12125  sumss  12127  fsum2dlem  12163  symgbas  14699  cntzval  14724  oppglsm  14880  efgval  14953  islss  15619  00lss  15626  mplsubglem  16106  ntrcls0  16740  neindisj2  16787  hauscmplem  17060  fbdmn0  17456  fbncp  17461  opnfbas  17464  fbasfip  17490  fbunfip  17491  fgcl  17500  supfil  17517  ufinffr  17551  alexsubALTlem2  17669  metnrmlem3  18292  itg1addlem4  18981  mdeg0  19383  uc1pval  19452  mon1pval  19454  pserulm  19725  derangsn  23038  vdgrun  23230  hdrmp  25038  coeq0i  26164  eldioph2lem2  26172  eldioph4b  26226  pcl0N  29241  pcl0bN  29242
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-dif 3097  df-in 3101  df-ss 3108  df-nul 3398
  Copyright terms: Public domain W3C validator