Theorem ss0 4355

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 4354	. 2 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)
2	1	biimpi 219	1 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)

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

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-dif 3905  df-ss 3919  df-nul 4283

This theorem is used by:  0dif  4359  eq0rdvALT  4369  ssdisj  4416  disjpss  4417  dfopif  4833  iunxdif3  5059  fr0  5637  poirr2  6122  sofld  6184  f00  6761  fvmptopab  7472  tfindsg  7861  findsg  7898  frxp  8128  map0b  8894  sbthlem7  9095  ssfi  9171  fi0  9394  cantnflem1  9672  rankeq0b  9846  scott0  9879  grur1a  10832  ixxdisj  13417  icodisj  13533  ioodisj  13539  uzdisj  13656  nn0disj  13703  hashf1lem2  14525  swrd0  14732  xptrrel  15057  sumz  15812  sumss  15814  fsum2dlem  15860  prod1  16037  prodss  16040  fprodss  16041  fprod2dlem  16073  cntzval  19454  oppglsm  19775  efgval  19850  islss  21124  00lss  21131  ssdifidllem  21553  mplsubglem  22219  ntrcls0  23307  neindisj2  23354  hauscmplem  23637  fbdmn0  24066  fbncp  24071  opnfbas  24074  fbasfip  24100  fbunfip  24101  fgcl  24110  supfil  24127  ufinffr  24161  alexsubALTlem2  24280  metnrmlem3  25094  itg1addlem4  25933  uc1pval  26372  mon1pval  26374  pserulm  26665  vtxdun  29949  vtxdginducedm1  30011  difres  33081  imadifxp  33082  swrdrndisj  33405  cycpmco2f1  33572  erlval  33706  ply1dg3rt0irred  34002  esumrnmpt2  34586  truae  34762  carsgclctunlem2  34838  acycgr0v  35735  prclisacycgr  35738  derangsn  35757  ttc00  37135  poimirlem3  38380  ismblfin  38418  pcl0N  40803  pcl0bN  40804  coeq0i  43606  eldioph2lem2  43614  eldioph4b  43660  oe0suclim  44126  ntrk2imkb  44885  ntrk0kbimka  44887  ssin0  45897  iccdifprioo  46354  sumnnodd  46468  sge0split  47245  iscnrm3llem2  49884  0setrec  50638