Theorem ss0 4368

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3917  ∅c0 4299

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-dif 3920  df-ss 3934  df-nul 4300

This theorem is referenced by:  sseq0  4369  0dif  4371  eq0rdvALT  4374  ssdisj  4426  disjpss  4427  dfopif  4837  iunxdif3  5062  fr0  5619  poirr2  6100  sofld  6163  f00  6745  fvmptopab  7446  tfindsg  7840  findsg  7876  frxp  8108  map0b  8859  sbthlem7  9063  ssfi  9143  fi0  9378  cantnflem1  9649  rankeq0b  9820  grur1a  10779  ixxdisj  13328  icodisj  13444  ioodisj  13450  uzdisj  13565  nn0disj  13612  hashf1lem2  14428  swrd0  14630  xptrrel  14953  sumz  15695  sumss  15697  fsum2dlem  15743  prod1  15917  prodss  15920  fprodss  15921  fprod2dlem  15953  cntzval  19260  oppglsm  19579  efgval  19654  islss  20847  00lss  20854  mplsubglem  21915  ntrcls0  22970  neindisj2  23017  hauscmplem  23300  fbdmn0  23728  fbncp  23733  opnfbas  23736  fbasfip  23762  fbunfip  23763  fgcl  23772  supfil  23789  ufinffr  23823  alexsubALTlem2  23942  metnrmlem3  24757  itg1addlem4  25607  uc1pval  26052  mon1pval  26054  pserulm  26338  vtxdun  29416  vtxdginducedm1  29478  difres  32536  imadifxp  32537  swrdrndisj  32886  cycpmco2f1  33088  erlval  33216  ssdifidllem  33434  ply1dg3rt0irred  33558  esumrnmpt2  34065  truae  34240  carsgclctunlem2  34317  acycgr0v  35142  prclisacycgr  35145  derangsn  35164  poimirlem3  37624  ismblfin  37662  pcl0N  39923  pcl0bN  39924  coeq0i  42748  eldioph2lem2  42756  eldioph4b  42806  oe0suclim  43273  ntrk2imkb  44033  ntrk0kbimka  44035  ssin0  45056  iccdifprioo  45521  sumnnodd  45635  sge0split  46414  iscnrm3llem2  48942  0setrec  49697