Theorem ss0 4407

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

Syntax hints:   → wi 4   = wceq 1536   ⊆ wss 3962  ∅c0 4338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-dif 3965  df-ss 3979  df-nul 4339

This theorem is referenced by:  sseq0  4408  0dif  4410  eq0rdvALT  4413  ssdisj  4465  disjpss  4466  dfopif  4874  iunxdif3  5099  fr0  5666  poirr2  6146  sofld  6208  f00  6790  fvmptopab  7486  tfindsg  7881  findsg  7919  frxp  8149  map0b  8921  sbthlem7  9127  ssfi  9211  phplem2OLD  9252  fi0  9457  cantnflem1  9726  rankeq0b  9897  grur1a  10856  ixxdisj  13398  icodisj  13512  ioodisj  13518  uzdisj  13633  nn0disj  13680  hashf1lem2  14491  swrd0  14692  xptrrel  15015  sumz  15754  sumss  15756  fsum2dlem  15802  prod1  15976  prodss  15979  fprodss  15980  fprod2dlem  16012  cntzval  19351  oppglsm  19674  efgval  19749  islss  20949  00lss  20956  mplsubglem  22036  ntrcls0  23099  neindisj2  23146  hauscmplem  23429  fbdmn0  23857  fbncp  23862  opnfbas  23865  fbasfip  23891  fbunfip  23892  fgcl  23901  supfil  23918  ufinffr  23952  alexsubALTlem2  24071  metnrmlem3  24896  itg1addlem4  25747  itg1addlem4OLD  25748  uc1pval  26193  mon1pval  26195  pserulm  26479  vtxdun  29513  vtxdginducedm1  29575  difres  32619  imadifxp  32620  swrdrndisj  32926  cycpmco2f1  33126  erlval  33244  ssdifidllem  33463  ply1dg3rt0irred  33586  esumrnmpt2  34048  truae  34223  carsgclctunlem2  34300  acycgr0v  35132  prclisacycgr  35135  derangsn  35154  poimirlem3  37609  ismblfin  37647  pcl0N  39904  pcl0bN  39905  coeq0i  42740  eldioph2lem2  42748  eldioph4b  42798  oe0suclim  43266  ntrk2imkb  44026  ntrk0kbimka  44028  ssin0  44994  iccdifprioo  45468  sumnnodd  45585  sge0split  46364  iscnrm3llem2  48746  0setrec  48934