Theorem ss0 4329

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3883  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900  df-nul 4254

This theorem is referenced by:  sseq0  4330  0dif  4332  eq0rdvALT  4336  ssdisj  4390  disjpss  4391  dfopifOLD  4798  iunxdif3  5020  fr0  5559  poirr2  6018  sofld  6079  f00  6640  tfindsg  7682  findsg  7720  frxp  7938  map0b  8629  sbthlem7  8829  phplem2  8893  ssfi  8918  fi0  9109  cantnflem1  9377  rankeq0b  9549  grur1a  10506  ixxdisj  13023  icodisj  13137  ioodisj  13143  uzdisj  13258  nn0disj  13301  hashf1lem2  14098  swrd0  14299  xptrrel  14619  sumz  15362  sumss  15364  fsum2dlem  15410  prod1  15582  prodss  15585  fprodss  15586  fprod2dlem  15618  cntzval  18842  oppglsm  19162  efgval  19238  islss  20111  00lss  20118  mplsubglem  21115  ntrcls0  22135  neindisj2  22182  hauscmplem  22465  fbdmn0  22893  fbncp  22898  opnfbas  22901  fbasfip  22927  fbunfip  22928  fgcl  22937  supfil  22954  ufinffr  22988  alexsubALTlem2  23107  metnrmlem3  23930  itg1addlem4  24768  itg1addlem4OLD  24769  uc1pval  25209  mon1pval  25211  pserulm  25486  vtxdun  27751  vtxdginducedm1  27813  difres  30840  imadifxp  30841  swrdrndisj  31131  cycpmco2f1  31293  esumrnmpt2  31936  truae  32111  carsgclctunlem2  32186  acycgr0v  33010  prclisacycgr  33013  derangsn  33032  poimirlem3  35707  ismblfin  35745  pcl0N  37863  pcl0bN  37864  coeq0i  40491  eldioph2lem2  40499  eldioph4b  40549  ntrk2imkb  41536  ntrk0kbimka  41538  ssin0  42492  iccdifprioo  42944  sumnnodd  43061  sge0split  43837  iscnrm3llem2  46132  0setrec  46295