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

Theorem ss0 3392
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 3391 . 2  |-  ( A 
C_  (/)  <->  A  =  (/) )
21biimpi 188 1  |-  ( A 
C_  (/)  ->  A  =  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619    C_ wss 3078   (/)c0 3362
This theorem is referenced by:  sseq0  3393  abf  3395  eq0rdv  3396  ssdisj  3411  disjpss  3412  0dif  3431  dfopif  3693  fr0  4265  tfindsg  4542  findsg  4574  poirr2  4974  sofld  5028  f00  5283  frxp  6077  map0b  6692  sbthlem7  6862  phplem2  6926  fi0  7057  cantnflem1  7275  rankeq0b  7416  grur1a  8321  ixxdisj  10549  icodisj  10639  ioodisj  10643  uzdisj  10734  hashf1lem2  11271  sumz  12072  sumss  12074  fsum2dlem  12110  symgbas  14607  cntzval  14632  oppglsm  14788  efgval  14861  islss  15527  00lss  15534  mplsubglem  16011  ntrcls0  16645  neindisj2  16692  hauscmplem  16965  fbdmn0  17361  fbncp  17366  opnfbas  17369  fbasfip  17395  fbunfip  17396  fgcl  17405  supfil  17422  ufinffr  17456  alexsubALTlem2  17574  metnrmlem3  18197  itg1addlem4  18886  mdeg0  19288  uc1pval  19357  mon1pval  19359  pserulm  19630  derangsn  22872  vdgrun  23064  hdrmp  24872  coeq0i  25998  eldioph2lem2  26006  eldioph4b  26060  pcl0N  28800  pcl0bN  28801
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-dif 3081  df-in 3085  df-ss 3089  df-nul 3363
  Copyright terms: Public domain W3C validator