Theorem ss0 4355

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3905  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-dif 3908  df-ss 3922  df-nul 4287

This theorem is referenced by:  sseq0  4356  0dif  4358  eq0rdvALT  4361  ssdisj  4413  disjpss  4414  dfopif  4824  iunxdif3  5047  fr0  5601  poirr2  6077  sofld  6140  f00  6710  fvmptopab  7408  tfindsg  7801  findsg  7837  frxp  8066  map0b  8817  sbthlem7  9017  ssfi  9097  fi0  9329  cantnflem1  9604  rankeq0b  9775  grur1a  10732  ixxdisj  13281  icodisj  13397  ioodisj  13403  uzdisj  13518  nn0disj  13565  hashf1lem2  14381  swrd0  14583  xptrrel  14905  sumz  15647  sumss  15649  fsum2dlem  15695  prod1  15869  prodss  15872  fprodss  15873  fprod2dlem  15905  cntzval  19218  oppglsm  19539  efgval  19614  islss  20855  00lss  20862  mplsubglem  21924  ntrcls0  22979  neindisj2  23026  hauscmplem  23309  fbdmn0  23737  fbncp  23742  opnfbas  23745  fbasfip  23771  fbunfip  23772  fgcl  23781  supfil  23798  ufinffr  23832  alexsubALTlem2  23951  metnrmlem3  24766  itg1addlem4  25616  uc1pval  26061  mon1pval  26063  pserulm  26347  vtxdun  29445  vtxdginducedm1  29507  difres  32562  imadifxp  32563  swrdrndisj  32912  cycpmco2f1  33079  erlval  33208  ssdifidllem  33403  ply1dg3rt0irred  33527  esumrnmpt2  34034  truae  34209  carsgclctunlem2  34286  acycgr0v  35120  prclisacycgr  35123  derangsn  35142  poimirlem3  37602  ismblfin  37640  pcl0N  39901  pcl0bN  39902  coeq0i  42726  eldioph2lem2  42734  eldioph4b  42784  oe0suclim  43250  ntrk2imkb  44010  ntrk0kbimka  44012  ssin0  45033  iccdifprioo  45498  sumnnodd  45612  sge0split  46391  iscnrm3llem2  48935  0setrec  49690