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

Theorem ss0 4359
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 (𝐴 ⊆ ∅ → 𝐴 = ∅)

Proof of Theorem ss0
StepHypRef Expression
1 ss0b 4358 . 2 (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)
21biimpi 215 1 (𝐴 ⊆ ∅ → 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wss 3911  c0 4283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-dif 3914  df-in 3918  df-ss 3928  df-nul 4284
This theorem is referenced by:  sseq0  4360  0dif  4362  eq0rdvALT  4366  ssdisj  4420  disjpss  4421  dfopif  4828  iunxdif3  5056  fr0  5613  poirr2  6079  sofld  6140  f00  6725  fvmptopab  7412  tfindsg  7798  findsg  7837  frxp  8059  map0b  8824  sbthlem7  9036  ssfi  9120  phplem2OLD  9165  fi0  9361  cantnflem1  9630  rankeq0b  9801  grur1a  10760  ixxdisj  13285  icodisj  13399  ioodisj  13405  uzdisj  13520  nn0disj  13563  hashf1lem2  14361  swrd0  14552  xptrrel  14871  sumz  15612  sumss  15614  fsum2dlem  15660  prod1  15832  prodss  15835  fprodss  15836  fprod2dlem  15868  cntzval  19106  oppglsm  19429  efgval  19504  islss  20410  00lss  20417  mplsubglem  21421  ntrcls0  22443  neindisj2  22490  hauscmplem  22773  fbdmn0  23201  fbncp  23206  opnfbas  23209  fbasfip  23235  fbunfip  23236  fgcl  23245  supfil  23262  ufinffr  23296  alexsubALTlem2  23415  metnrmlem3  24240  itg1addlem4  25079  itg1addlem4OLD  25080  uc1pval  25520  mon1pval  25522  pserulm  25797  vtxdun  28471  vtxdginducedm1  28533  difres  31564  imadifxp  31565  swrdrndisj  31860  cycpmco2f1  32022  esumrnmpt2  32724  truae  32899  carsgclctunlem2  32976  acycgr0v  33799  prclisacycgr  33802  derangsn  33821  poimirlem3  36127  ismblfin  36165  pcl0N  38431  pcl0bN  38432  coeq0i  41119  eldioph2lem2  41127  eldioph4b  41177  oe0suclim  41655  ntrk2imkb  42397  ntrk0kbimka  42399  ssin0  43351  iccdifprioo  43840  sumnnodd  43957  sge0split  44736  iscnrm3llem2  47069  0setrec  47235
  Copyright terms: Public domain W3C validator