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

Theorem ss0 4007
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 4006 . 2 (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)
21biimpi 206 1 (𝐴 ⊆ ∅ → 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wss 3607  c0 3948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-in 3614  df-ss 3621  df-nul 3949
This theorem is referenced by:  sseq0  4008  0dif  4010  eq0rdv  4012  ssdisj  4059  ssdisjOLD  4060  disjpss  4061  dfopif  4430  iunxdif3  4638  fr0  5122  poirr2  5555  sofld  5616  f00  6125  tfindsg  7102  findsg  7135  frxp  7332  map0b  7938  sbthlem7  8117  phplem2  8181  fi0  8367  cantnflem1  8624  rankeq0b  8761  grur1a  9679  ixxdisj  12228  icodisj  12335  ioodisj  12340  uzdisj  12451  nn0disj  12494  hashf1lem2  13278  swrd0  13480  xptrrel  13765  sumz  14497  sumss  14499  fsum2dlem  14545  prod1  14718  prodss  14721  fprodss  14722  fprod2dlem  14754  cntzval  17800  symgbas  17846  oppglsm  18103  efgval  18176  islss  18983  00lss  18990  mplsubglem  19482  ntrcls0  20928  neindisj2  20975  hauscmplem  21257  fbdmn0  21685  fbncp  21690  opnfbas  21693  fbasfip  21719  fbunfip  21720  fgcl  21729  supfil  21746  ufinffr  21780  alexsubALTlem2  21899  metnrmlem3  22711  itg1addlem4  23511  uc1pval  23944  mon1pval  23946  pserulm  24221  vtxdun  26433  vtxdginducedm1  26495  difres  29539  imadifxp  29540  esumrnmpt2  30258  truae  30434  carsgclctunlem2  30509  derangsn  31278  poimirlem3  33542  ismblfin  33580  pcl0N  35526  pcl0bN  35527  coeq0i  37633  eldioph2lem2  37641  eldioph4b  37692  ntrk2imkb  38652  ntrk0kbimka  38654  ssin0  39537  iccdifprioo  40060  sumnnodd  40180  sge0split  40944  0setrec  42775
  Copyright terms: Public domain W3C validator