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

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

Syntax hints:   → wi 4   = wceq 1563   ⊆ wss 3907  ∅c0 4288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-dif 3910  df-ss 3924  df-nul 4289

This theorem is referenced by:  sseq0  4360  0dif  4362  eq0rdvALT  4365  ssdisj  4417  disjpss  4418  dfopif  4831  iunxdif3  5057  fr0  5630  poirr2  6115  sofld  6177  f00  6750  fvmptopab  7455  tfindsg  7845  findsg  7882  frxp  8110  map0b  8869  sbthlem7  9069  ssfi  9145  fi0  9368  cantnflem1  9646  rankeq0b  9820  grur1a  10792  ixxdisj  13378  icodisj  13494  ioodisj  13500  uzdisj  13616  nn0disj  13663  hashf1lem2  14483  swrd0  14686  xptrrel  15007  sumz  15763  sumss  15765  fsum2dlem  15811  prod1  15988  prodss  15991  fprodss  15992  fprod2dlem  16024  cntzval  19382  oppglsm  19703  efgval  19778  islss  21024  00lss  21031  ssdifidllem  21444  mplsubglem  22108  ntrcls0  23194  neindisj2  23241  hauscmplem  23524  fbdmn0  23952  fbncp  23957  opnfbas  23960  fbasfip  23986  fbunfip  23987  fgcl  23996  supfil  24013  ufinffr  24047  alexsubALTlem2  24166  metnrmlem3  24980  itg1addlem4  25819  uc1pval  26258  mon1pval  26260  pserulm  26543  vtxdun  29740  vtxdginducedm1  29802  difres  32855  imadifxp  32856  swrdrndisj  33190  cycpmco2f1  33357  erlval  33491  ply1dg3rt0irred  33791  esumrnmpt2  34375  truae  34550  carsgclctunlem2  34626  acycgr0v  35511  prclisacycgr  35514  derangsn  35533  ttc00  36881  poimirlem3  38134  ismblfin  38172  pcl0N  40558  pcl0bN  40559  coeq0i  43346  eldioph2lem2  43354  eldioph4b  43400  oe0suclim  43866  ntrk2imkb  44625  ntrk0kbimka  44627  ssin0  45633  iccdifprioo  46090  sumnnodd  46204  sge0split  46981  iscnrm3llem2  49579  0setrec  50333