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

Theorem ss0 3658
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 3657 . 2  |-  ( A 
C_  (/)  <->  A  =  (/) )
21biimpi 187 1  |-  ( A 
C_  (/)  ->  A  =  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    C_ wss 3320   (/)c0 3628
This theorem is referenced by:  sseq0  3659  abf  3661  eq0rdv  3662  ssdisj  3677  disjpss  3678  0dif  3699  dfopif  3981  fr0  4561  tfindsg  4840  findsg  4872  poirr2  5258  sofld  5318  f00  5628  frxp  6456  map0b  7052  sbthlem7  7223  phplem2  7287  fi0  7425  cantnflem1  7645  rankeq0b  7786  grur1a  8694  ixxdisj  10931  icodisj  11022  ioodisj  11026  uzdisj  11119  hashf1lem2  11705  sumz  12516  sumss  12518  fsum2dlem  12554  symgbas  15095  cntzval  15120  oppglsm  15276  efgval  15349  islss  16011  00lss  16018  mplsubglem  16498  ntrcls0  17140  neindisj2  17187  hauscmplem  17469  fbdmn0  17866  fbncp  17871  opnfbas  17874  fbasfip  17900  fbunfip  17901  fgcl  17910  supfil  17927  ufinffr  17961  alexsubALTlem2  18079  metnrmlem3  18891  itg1addlem4  19591  mdeg0  19993  uc1pval  20062  mon1pval  20064  pserulm  20338  vdgrun  21672  vdgrfiun  21673  imadifxp  24038  measunl  24570  truae  24594  derangsn  24856  prod1  25270  prodss  25273  fprodss  25274  fprod2dlem  25304  ismblfin  26247  coeq0i  26811  eldioph2lem2  26819  eldioph4b  26872  pcl0N  30719  pcl0bN  30720
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-dif 3323  df-in 3327  df-ss 3334  df-nul 3629
  Copyright terms: Public domain W3C validator