Theorem ss0 4342

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3889  ∅c0 4273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-dif 3892  df-ss 3906  df-nul 4274

This theorem is referenced by:  sseq0  4343  0dif  4345  eq0rdvALT  4348  ssdisj  4400  disjpss  4401  dfopif  4813  iunxdif3  5037  fr0  5609  poirr2  6087  sofld  6151  f00  6722  fvmptopab  7422  tfindsg  7812  findsg  7848  frxp  8076  map0b  8831  sbthlem7  9031  ssfi  9107  fi0  9333  cantnflem1  9610  rankeq0b  9784  grur1a  10742  ixxdisj  13313  icodisj  13429  ioodisj  13435  uzdisj  13551  nn0disj  13598  hashf1lem2  14418  swrd0  14621  xptrrel  14942  sumz  15684  sumss  15686  fsum2dlem  15732  prod1  15909  prodss  15912  fprodss  15913  fprod2dlem  15945  cntzval  19296  oppglsm  19617  efgval  19692  islss  20929  00lss  20936  mplsubglem  21977  ntrcls0  23041  neindisj2  23088  hauscmplem  23371  fbdmn0  23799  fbncp  23804  opnfbas  23807  fbasfip  23833  fbunfip  23834  fgcl  23843  supfil  23860  ufinffr  23894  alexsubALTlem2  24013  metnrmlem3  24827  itg1addlem4  25666  uc1pval  26105  mon1pval  26107  pserulm  26387  vtxdun  29550  vtxdginducedm1  29612  difres  32670  imadifxp  32671  swrdrndisj  33017  cycpmco2f1  33185  erlval  33319  ssdifidllem  33516  ply1dg3rt0irred  33644  esumrnmpt2  34212  truae  34387  carsgclctunlem2  34463  acycgr0v  35330  prclisacycgr  35333  derangsn  35352  ttc00  36690  poimirlem3  37944  ismblfin  37982  pcl0N  40368  pcl0bN  40369  coeq0i  43185  eldioph2lem2  43193  eldioph4b  43239  oe0suclim  43705  ntrk2imkb  44464  ntrk0kbimka  44466  ssin0  45486  iccdifprioo  45946  sumnnodd  46060  sge0split  46837  iscnrm3llem2  49425  0setrec  50179