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

Theorem ss0 3487
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 3486 . 2  |-  ( A 
C_  (/)  <->  A  =  (/) )
21biimpi 186 1  |-  ( A 
C_  (/)  ->  A  =  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625    C_ wss 3154   (/)c0 3457
This theorem is referenced by:  sseq0  3488  abf  3490  eq0rdv  3491  ssdisj  3506  disjpss  3507  0dif  3527  dfopif  3795  fr0  4374  tfindsg  4653  findsg  4685  poirr2  5069  sofld  5123  f00  5428  frxp  6227  map0b  6808  sbthlem7  6979  phplem2  7043  fi0  7175  cantnflem1  7393  rankeq0b  7534  grur1a  8443  ixxdisj  10673  icodisj  10763  ioodisj  10767  uzdisj  10858  hashf1lem2  11396  sumz  12197  sumss  12199  fsum2dlem  12235  symgbas  14774  cntzval  14799  oppglsm  14955  efgval  15028  islss  15694  00lss  15701  mplsubglem  16181  ntrcls0  16815  neindisj2  16862  hauscmplem  17135  fbdmn0  17531  fbncp  17536  opnfbas  17539  fbasfip  17565  fbunfip  17566  fgcl  17575  supfil  17592  ufinffr  17626  alexsubALTlem2  17744  metnrmlem3  18367  itg1addlem4  19056  mdeg0  19458  uc1pval  19527  mon1pval  19529  pserulm  19800  derangsn  23703  vdgrun  23895  hdrmp  25717  coeq0i  26843  eldioph2lem2  26851  eldioph4b  26905  pcl0N  30184  pcl0bN  30185
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-dif 3157  df-in 3161  df-ss 3168  df-nul 3458
  Copyright terms: Public domain W3C validator