Theorem ss0 3974

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

Syntax hints:   → wi 4   = wceq 1483   ⊆ wss 3574  ∅c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588  df-nul 3916

This theorem is referenced by:  sseq0  3975  0dif  3977  eq0rdv  3979  ssdisj  4026  ssdisjOLD  4027  disjpss  4028  dfopif  4399  iunxdif3  4606  fr0  5093  poirr2  5520  sofld  5581  f00  6087  tfindsg  7060  findsg  7093  frxp  7287  map0b  7896  sbthlem7  8076  phplem2  8140  fi0  8326  cantnflem1  8586  rankeq0b  8723  grur1a  9641  ixxdisj  12190  icodisj  12297  ioodisj  12302  uzdisj  12413  nn0disj  12455  hashf1lem2  13240  swrd0  13434  xptrrel  13719  sumz  14453  sumss  14455  fsum2dlem  14501  prod1  14674  prodss  14677  fprodss  14678  fprod2dlem  14710  cntzval  17754  symgbas  17800  oppglsm  18057  efgval  18130  islss  18935  00lss  18942  mplsubglem  19434  ntrcls0  20880  neindisj2  20927  hauscmplem  21209  fbdmn0  21638  fbncp  21643  opnfbas  21646  fbasfip  21672  fbunfip  21673  fgcl  21682  supfil  21699  ufinffr  21733  alexsubALTlem2  21852  metnrmlem3  22664  itg1addlem4  23466  uc1pval  23899  mon1pval  23901  pserulm  24176  vtxdun  26377  vtxdginducedm1  26439  difres  29413  imadifxp  29414  esumrnmpt2  30130  truae  30306  carsgclctunlem2  30381  derangsn  31152  poimirlem3  33412  ismblfin  33450  opabf  34131  pcl0N  35208  pcl0bN  35209  coeq0i  37316  eldioph2lem2  37324  eldioph4b  37375  ntrk2imkb  38335  ntrk0kbimka  38337  ssin0  39223  iccdifprioo  39742  sumnnodd  39862  sge0split  40626  0setrec  42447