Theorem ss0 4362

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3908  ∅c0 4289

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-dif 3911  df-ss 3925  df-nul 4290

This theorem is used by:  0dif  4366  eq0rdvALT  4376  ssdisj  4423  disjpss  4424  dfopif  4840  iunxdif3  5066  fr0  5644  poirr2  6129  sofld  6190  f00  6767  fvmptopab  7478  tfindsg  7866  findsg  7903  frxp  8131  map0b  8890  sbthlem7  9091  ssfi  9167  fi0  9390  cantnflem1  9668  rankeq0b  9842  scott0  9875  grur1a  10822  ixxdisj  13405  icodisj  13521  ioodisj  13527  uzdisj  13644  nn0disj  13691  hashf1lem2  14513  swrd0  14720  xptrrel  15043  sumz  15799  sumss  15801  fsum2dlem  15847  prod1  16024  prodss  16027  fprodss  16028  fprod2dlem  16060  cntzval  19422  oppglsm  19743  efgval  19818  islss  21092  00lss  21099  ssdifidllem  21521  mplsubglem  22185  ntrcls0  23270  neindisj2  23317  hauscmplem  23600  fbdmn0  24028  fbncp  24033  opnfbas  24036  fbasfip  24062  fbunfip  24063  fgcl  24072  supfil  24089  ufinffr  24123  alexsubALTlem2  24242  metnrmlem3  25056  itg1addlem4  25895  uc1pval  26334  mon1pval  26336  pserulm  26622  vtxdun  29868  vtxdginducedm1  29930  difres  32982  imadifxp  32983  swrdrndisj  33308  cycpmco2f1  33475  erlval  33609  ply1dg3rt0irred  33905  esumrnmpt2  34489  truae  34664  carsgclctunlem2  34740  acycgr0v  35660  prclisacycgr  35663  derangsn  35682  ttc00  37059  poimirlem3  38314  ismblfin  38352  pcl0N  40736  pcl0bN  40737  coeq0i  43524  eldioph2lem2  43532  eldioph4b  43578  oe0suclim  44044  ntrk2imkb  44803  ntrk0kbimka  44805  ssin0  45815  iccdifprioo  46272  sumnnodd  46386  sge0split  47163  iscnrm3llem2  49768  0setrec  50522