Theorem ss0 4297

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3853  ∅c0 4221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3402  df-dif 3856  df-in 3860  df-ss 3870  df-nul 4222

This theorem is referenced by:  sseq0  4298  0dif  4300  eq0rdvALT  4304  ssdisj  4359  disjpss  4360  dfopifOLD  4766  iunxdif3  4990  fr0  5514  poirr2  5968  sofld  6029  f00  6571  tfindsg  7607  findsg  7643  frxp  7859  map0b  8506  sbthlem7  8696  phplem2  8760  ssfi  8785  fi0  8970  cantnflem1  9238  rankeq0b  9375  grur1a  10332  ixxdisj  12849  icodisj  12963  ioodisj  12969  uzdisj  13084  nn0disj  13127  hashf1lem2  13921  swrd0  14122  xptrrel  14442  sumz  15185  sumss  15187  fsum2dlem  15231  prod1  15403  prodss  15406  fprodss  15407  fprod2dlem  15439  cntzval  18582  oppglsm  18898  efgval  18974  islss  19838  00lss  19845  mplsubglem  20828  ntrcls0  21840  neindisj2  21887  hauscmplem  22170  fbdmn0  22598  fbncp  22603  opnfbas  22606  fbasfip  22632  fbunfip  22633  fgcl  22642  supfil  22659  ufinffr  22693  alexsubALTlem2  22812  metnrmlem3  23626  itg1addlem4  24464  itg1addlem4OLD  24465  uc1pval  24905  mon1pval  24907  pserulm  25182  vtxdun  27436  vtxdginducedm1  27498  difres  30526  imadifxp  30527  swrdrndisj  30817  cycpmco2f1  30981  esumrnmpt2  31619  truae  31794  carsgclctunlem2  31869  acycgr0v  32694  prclisacycgr  32697  derangsn  32716  poimirlem3  35436  ismblfin  35474  pcl0N  37592  pcl0bN  37593  coeq0i  40188  eldioph2lem2  40196  eldioph4b  40246  ntrk2imkb  41234  ntrk0kbimka  41236  ssin0  42182  iccdifprioo  42635  sumnnodd  42754  sge0split  43530  iscnrm3llem2  45814  0setrec  45910