Theorem ss0 4398

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3948  ∅c0 4322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3951  df-in 3955  df-ss 3965  df-nul 4323

This theorem is referenced by:  sseq0  4399  0dif  4401  eq0rdvALT  4405  ssdisj  4459  disjpss  4460  dfopif  4870  iunxdif3  5098  fr0  5655  poirr2  6125  sofld  6186  f00  6773  fvmptopab  7462  tfindsg  7849  findsg  7889  frxp  8111  map0b  8876  sbthlem7  9088  ssfi  9172  phplem2OLD  9217  fi0  9414  cantnflem1  9683  rankeq0b  9854  grur1a  10813  ixxdisj  13338  icodisj  13452  ioodisj  13458  uzdisj  13573  nn0disj  13616  hashf1lem2  14416  swrd0  14607  xptrrel  14926  sumz  15667  sumss  15669  fsum2dlem  15715  prod1  15887  prodss  15890  fprodss  15891  fprod2dlem  15923  cntzval  19184  oppglsm  19509  efgval  19584  islss  20544  00lss  20551  mplsubglem  21557  ntrcls0  22579  neindisj2  22626  hauscmplem  22909  fbdmn0  23337  fbncp  23342  opnfbas  23345  fbasfip  23371  fbunfip  23372  fgcl  23381  supfil  23398  ufinffr  23432  alexsubALTlem2  23551  metnrmlem3  24376  itg1addlem4  25215  itg1addlem4OLD  25216  uc1pval  25656  mon1pval  25658  pserulm  25933  vtxdun  28735  vtxdginducedm1  28797  difres  31826  imadifxp  31827  swrdrndisj  32116  cycpmco2f1  32278  esumrnmpt2  33061  truae  33236  carsgclctunlem2  33313  acycgr0v  34134  prclisacycgr  34137  derangsn  34156  poimirlem3  36486  ismblfin  36524  pcl0N  38788  pcl0bN  38789  coeq0i  41481  eldioph2lem2  41489  eldioph4b  41539  oe0suclim  42017  ntrk2imkb  42778  ntrk0kbimka  42780  ssin0  43732  iccdifprioo  44219  sumnnodd  44336  sge0split  45115  iscnrm3llem2  47573  0setrec  47739