Theorem ss0 4352

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

Step	Hyp	Ref	Expression
1		ss0b 4351	. 2 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)
2	1	biimpi 219	1 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-dif 3902  df-ss 3916  df-nul 4280

This theorem is used by:  0dif  4356  eq0rdvALT  4366  ssdisj  4413  disjpss  4414  dfopif  4830  iunxdif3  5055  fr0  5629  poirr2  6116  sofld  6178  f00  6756  fvmptopab  7467  tfindsg  7861  findsg  7898  frxp  8127  map0b  8895  sbthlem7  9096  ssfi  9172  fi0  9396  cantnflem1  9674  rankeq0b  9857  scott0  9917  grur1a  10885  ixxdisj  13472  icodisj  13588  ioodisj  13594  uzdisj  13711  nn0disj  13758  hashf1lem2  14581  swrd0  14788  xptrrel  15113  sumz  15868  sumss  15870  fsum2dlem  15916  prod1  16091  prodss  16094  fprodss  16095  fprod2dlem  16127  cntzval  19515  oppglsm  19836  efgval  19911  islss  21189  00lss  21196  ssdifidllem  21620  mplsubglem  22286  ntrcls0  23374  neindisj2  23421  hauscmplem  23704  fbdmn0  24133  fbncp  24138  opnfbas  24141  fbasfip  24167  fbunfip  24168  fgcl  24177  supfil  24194  ufinffr  24228  alexsubALTlem2  24347  metnrmlem3  25161  itg1addlem4  26000  uc1pval  26438  mon1pval  26440  pserulm  26731  vtxdun  30044  vtxdginducedm1  30106  difres  33176  imadifxp  33177  swrdrndisj  33500  cycpmco2f1  33667  erlval  33801  ply1dg3rt0irred  34098  esumrnmpt2  34682  truae  34858  carsgclctunlem2  34934  acycgr0v  35882  prclisacycgr  35885  derangsn  35904  ttc00  37266  poimirlem3  38509  ismblfin  38547  pcl0N  40947  pcl0bN  40948  coeq0i  43717  eldioph2lem2  43725  eldioph4b  43771  oe0suclim  44237  ntrk2imkb  44996  ntrk0kbimka  44998  ssin0  46015  iccdifprioo  46472  sumnnodd  46586  sge0split  47363  iscnrm3llem2  50002  0setrec  50741