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

Theorem ss0 3595
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 3594 . 2  |-  ( A 
C_  (/)  <->  A  =  (/) )
21biimpi 187 1  |-  ( A 
C_  (/)  ->  A  =  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    C_ wss 3257   (/)c0 3565
This theorem is referenced by:  sseq0  3596  abf  3598  eq0rdv  3599  ssdisj  3614  disjpss  3615  0dif  3636  dfopif  3917  fr0  4496  tfindsg  4774  findsg  4806  poirr2  5192  sofld  5252  f00  5562  frxp  6386  map0b  6982  sbthlem7  7153  phplem2  7217  fi0  7354  cantnflem1  7572  rankeq0b  7713  grur1a  8621  ixxdisj  10857  icodisj  10948  ioodisj  10952  uzdisj  11043  hashf1lem2  11626  sumz  12437  sumss  12439  fsum2dlem  12475  symgbas  15016  cntzval  15041  oppglsm  15197  efgval  15270  islss  15932  00lss  15939  mplsubglem  16419  ntrcls0  17057  neindisj2  17104  hauscmplem  17385  fbdmn0  17781  fbncp  17786  opnfbas  17789  fbasfip  17815  fbunfip  17816  fgcl  17825  supfil  17842  ufinffr  17876  alexsubALTlem2  17994  metnrmlem3  18756  itg1addlem4  19452  mdeg0  19854  uc1pval  19923  mon1pval  19925  pserulm  20199  vdgrun  21514  vdgrfiun  21515  imadifxp  23875  measunl  24358  truae  24382  derangsn  24629  prod1  25043  prodss  25046  fprodss  25047  coeq0i  26496  eldioph2lem2  26504  eldioph4b  26557  pcl0N  30088  pcl0bN  30089
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2362
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2506  df-v 2895  df-dif 3260  df-in 3264  df-ss 3271  df-nul 3566
  Copyright terms: Public domain W3C validator