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

Theorem ss0 4356
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 4355 . 2 (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)
21biimpi 217 1 (𝐴 ⊆ ∅ → 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wss 3940  c0 4295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-dif 3943  df-in 3947  df-ss 3956  df-nul 4296
This theorem is referenced by:  sseq0  4357  0dif  4359  eq0rdv  4361  ssdisj  4412  disjpss  4413  dfopif  4799  iunxdif3  5014  fr0  5533  poirr2  5982  sofld  6042  f00  6558  tfindsg  7563  findsg  7597  frxp  7811  map0b  8437  sbthlem7  8622  phplem2  8686  fi0  8873  cantnflem1  9141  rankeq0b  9278  grur1a  10230  ixxdisj  12743  icodisj  12852  ioodisj  12858  uzdisj  12970  nn0disj  13013  hashf1lem2  13804  swrd0  14010  xptrrel  14330  sumz  15069  sumss  15071  fsum2dlem  15115  prod1  15288  prodss  15291  fprodss  15292  fprod2dlem  15324  cntzval  18381  symgbas  18428  oppglsm  18687  efgval  18763  islss  19626  00lss  19633  mplsubglem  20133  ntrcls0  21600  neindisj2  21647  hauscmplem  21930  fbdmn0  22358  fbncp  22363  opnfbas  22366  fbasfip  22392  fbunfip  22393  fgcl  22402  supfil  22419  ufinffr  22453  alexsubALTlem2  22572  metnrmlem3  23384  itg1addlem4  24215  uc1pval  24648  mon1pval  24650  pserulm  24925  vtxdun  27177  vtxdginducedm1  27239  difres  30265  imadifxp  30266  swrdrndisj  30545  cycpmco2f1  30680  esumrnmpt2  31213  truae  31388  carsgclctunlem2  31463  acycgr0v  32279  prclisacycgr  32282  derangsn  32301  poimirlem3  34762  ismblfin  34800  pcl0N  36925  pcl0bN  36926  coeq0i  39215  eldioph2lem2  39223  eldioph4b  39273  ntrk2imkb  40252  ntrk0kbimka  40254  ssin0  41182  iccdifprioo  41657  sumnnodd  41776  sge0split  42557  0setrec  44638
  Copyright terms: Public domain W3C validator