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 218	1 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)

Syntax hints:   → wi 4   = wceq 1559   ⊆ wss 3904  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-dif 3907  df-ss 3921  df-nul 4286

This theorem is referenced by:  sseq0  4356  0dif  4358  eq0rdvALT  4361  ssdisj  4413  disjpss  4414  dfopif  4827  iunxdif3  5051  fr0  5623  poirr2  6108  sofld  6169  f00  6742  fvmptopab  7447  tfindsg  7837  findsg  7874  frxp  8101  map0b  8861  sbthlem7  9061  ssfi  9137  fi0  9363  cantnflem1  9641  rankeq0b  9815  grur1a  10774  ixxdisj  13361  icodisj  13477  ioodisj  13483  uzdisj  13599  nn0disj  13646  hashf1lem2  14466  swrd0  14669  xptrrel  14990  sumz  15732  sumss  15734  fsum2dlem  15780  prod1  15957  prodss  15960  fprodss  15961  fprod2dlem  15993  cntzval  19344  oppglsm  19665  efgval  19740  islss  20981  00lss  20988  mplsubglem  22030  ntrcls0  23116  neindisj2  23163  hauscmplem  23446  fbdmn0  23874  fbncp  23879  opnfbas  23882  fbasfip  23908  fbunfip  23909  fgcl  23918  supfil  23935  ufinffr  23969  alexsubALTlem2  24088  metnrmlem3  24902  itg1addlem4  25741  uc1pval  26180  mon1pval  26182  pserulm  26462  vtxdun  29628  vtxdginducedm1  29690  difres  32749  imadifxp  32750  swrdrndisj  33096  cycpmco2f1  33265  erlval  33400  ssdifidllem  33604  ply1dg3rt0irred  33741  esumrnmpt2  34326  truae  34501  carsgclctunlem2  34577  acycgr0v  35462  prclisacycgr  35465  derangsn  35484  ttc00  36832  poimirlem3  38086  ismblfin  38124  pcl0N  40510  pcl0bN  40511  coeq0i  43298  eldioph2lem2  43306  eldioph4b  43352  oe0suclim  43818  ntrk2imkb  44577  ntrk0kbimka  44579  ssin0  45599  iccdifprioo  46056  sumnnodd  46170  sge0split  46947  iscnrm3llem2  49535  0setrec  50289