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 216	1 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3902  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-dif 3905  df-ss 3919  df-nul 4284

This theorem is referenced by:  sseq0  4353  0dif  4355  eq0rdvALT  4358  ssdisj  4410  disjpss  4411  dfopif  4822  iunxdif3  5043  fr0  5594  poirr2  6071  sofld  6134  f00  6705  fvmptopab  7401  tfindsg  7791  findsg  7827  frxp  8056  map0b  8807  sbthlem7  9006  ssfi  9082  fi0  9304  cantnflem1  9579  rankeq0b  9750  grur1a  10707  ixxdisj  13257  icodisj  13373  ioodisj  13379  uzdisj  13494  nn0disj  13541  hashf1lem2  14360  swrd0  14563  xptrrel  14884  sumz  15626  sumss  15628  fsum2dlem  15674  prod1  15848  prodss  15851  fprodss  15852  fprod2dlem  15884  cntzval  19231  oppglsm  19552  efgval  19627  islss  20865  00lss  20872  mplsubglem  21934  ntrcls0  22989  neindisj2  23036  hauscmplem  23319  fbdmn0  23747  fbncp  23752  opnfbas  23755  fbasfip  23781  fbunfip  23782  fgcl  23791  supfil  23808  ufinffr  23842  alexsubALTlem2  23961  metnrmlem3  24775  itg1addlem4  25625  uc1pval  26070  mon1pval  26072  pserulm  26356  vtxdun  29458  vtxdginducedm1  29520  difres  32575  imadifxp  32576  swrdrndisj  32933  cycpmco2f1  33088  erlval  33220  ssdifidllem  33416  ply1dg3rt0irred  33541  esumrnmpt2  34076  truae  34251  carsgclctunlem2  34327  acycgr0v  35180  prclisacycgr  35183  derangsn  35202  poimirlem3  37662  ismblfin  37700  pcl0N  39960  pcl0bN  39961  coeq0i  42785  eldioph2lem2  42793  eldioph4b  42843  oe0suclim  43309  ntrk2imkb  44069  ntrk0kbimka  44071  ssin0  45091  iccdifprioo  45555  sumnnodd  45669  sge0split  46446  iscnrm3llem2  48980  0setrec  49735