Theorem ss0 3946

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

Syntax hints:   → wi 4   = wceq 1480   ⊆ wss 3555  ∅c0 3891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-dif 3558  df-in 3562  df-ss 3569  df-nul 3892

This theorem is referenced by:  sseq0  3947  0dif  3949  eq0rdv  3951  ssdisj  3998  ssdisjOLD  3999  disjpss  4000  dfopif  4367  iunxdif3  4572  fr0  5053  poirr2  5479  sofld  5540  f00  6044  tfindsg  7007  findsg  7040  frxp  7232  map0b  7840  sbthlem7  8020  phplem2  8084  fi0  8270  cantnflem1  8530  rankeq0b  8667  grur1a  9585  ixxdisj  12132  icodisj  12239  ioodisj  12244  uzdisj  12354  nn0disj  12396  hashf1lem2  13178  swrd0  13372  xptrrel  13653  sumz  14386  sumss  14388  fsum2dlem  14429  prod1  14599  prodss  14602  fprodss  14603  fprod2dlem  14635  cntzval  17675  symgbas  17721  oppglsm  17978  efgval  18051  islss  18854  00lss  18861  mplsubglem  19353  ntrcls0  20790  neindisj2  20837  hauscmplem  21119  fbdmn0  21548  fbncp  21553  opnfbas  21556  fbasfip  21582  fbunfip  21583  fgcl  21592  supfil  21609  ufinffr  21643  alexsubALTlem2  21762  metnrmlem3  22572  itg1addlem4  23372  uc1pval  23803  mon1pval  23805  pserulm  24080  vtxdun  26263  difres  29255  imadifxp  29256  esumrnmpt2  29908  truae  30084  carsgclctunlem2  30159  derangsn  30857  poimirlem3  33041  ismblfin  33079  pcl0N  34685  pcl0bN  34686  coeq0i  36793  eldioph2lem2  36801  eldioph4b  36852  ntrk2imkb  37814  ntrk0kbimka  37816  ssin0  38705  iccdifprioo  39150  sumnnodd  39263  sge0split  39930  0setrec  41737