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

Theorem ss0 3460
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 3459 . 2  |-  ( A 
C_  (/)  <->  A  =  (/) )
21biimpi 188 1  |-  ( A 
C_  (/)  ->  A  =  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619    C_ wss 3127   (/)c0 3430
This theorem is referenced by:  sseq0  3461  abf  3463  eq0rdv  3464  ssdisj  3479  disjpss  3480  0dif  3500  dfopif  3767  fr0  4344  tfindsg  4623  findsg  4655  poirr2  5055  sofld  5109  f00  5364  frxp  6159  map0b  6774  sbthlem7  6945  phplem2  7009  fi0  7141  cantnflem1  7359  rankeq0b  7500  grur1a  8409  ixxdisj  10638  icodisj  10728  ioodisj  10732  uzdisj  10823  hashf1lem2  11360  sumz  12161  sumss  12163  fsum2dlem  12199  symgbas  14735  cntzval  14760  oppglsm  14916  efgval  14989  islss  15655  00lss  15662  mplsubglem  16142  ntrcls0  16776  neindisj2  16823  hauscmplem  17096  fbdmn0  17492  fbncp  17497  opnfbas  17500  fbasfip  17526  fbunfip  17527  fgcl  17536  supfil  17553  ufinffr  17587  alexsubALTlem2  17705  metnrmlem3  18328  itg1addlem4  19017  mdeg0  19419  uc1pval  19488  mon1pval  19490  pserulm  19761  derangsn  23074  vdgrun  23266  hdrmp  25074  coeq0i  26200  eldioph2lem2  26208  eldioph4b  26262  pcl0N  29361  pcl0bN  29362
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 2239
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 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-dif 3130  df-in 3134  df-ss 3141  df-nul 3431
  Copyright terms: Public domain W3C validator