Theorem ss0 4346

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

Syntax hints:   → wi 4   = wceq 1550   ⊆ wss 3895  ∅c0 4276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-dif 3898  df-ss 3912  df-nul 4277

This theorem is referenced by:  sseq0  4347  0dif  4349  eq0rdvALT  4352  ssdisj  4404  disjpss  4405  dfopif  4818  iunxdif3  5042  fr0  5614  poirr2  6097  sofld  6158  f00  6731  fvmptopab  7436  tfindsg  7826  findsg  7863  frxp  8090  map0b  8850  sbthlem7  9050  ssfi  9126  fi0  9352  cantnflem1  9630  rankeq0b  9804  grur1a  10763  ixxdisj  13350  icodisj  13466  ioodisj  13472  uzdisj  13588  nn0disj  13635  hashf1lem2  14455  swrd0  14658  xptrrel  14979  sumz  15721  sumss  15723  fsum2dlem  15769  prod1  15946  prodss  15949  fprodss  15950  fprod2dlem  15982  cntzval  19333  oppglsm  19654  efgval  19729  islss  20970  00lss  20977  mplsubglem  22019  ntrcls0  23105  neindisj2  23152  hauscmplem  23435  fbdmn0  23863  fbncp  23868  opnfbas  23871  fbasfip  23897  fbunfip  23898  fgcl  23907  supfil  23924  ufinffr  23958  alexsubALTlem2  24077  metnrmlem3  24891  itg1addlem4  25730  uc1pval  26169  mon1pval  26171  pserulm  26451  vtxdun  29617  vtxdginducedm1  29679  difres  32738  imadifxp  32739  swrdrndisj  33085  cycpmco2f1  33254  erlval  33388  ssdifidllem  33588  ply1dg3rt0irred  33724  esumrnmpt2  34309  truae  34484  carsgclctunlem2  34560  acycgr0v  35436  prclisacycgr  35439  derangsn  35458  ttc00  36806  poimirlem3  38060  ismblfin  38098  pcl0N  40484  pcl0bN  40485  coeq0i  43272  eldioph2lem2  43280  eldioph4b  43326  oe0suclim  43792  ntrk2imkb  44551  ntrk0kbimka  44553  ssin0  45573  iccdifprioo  46030  sumnnodd  46144  sge0split  46921  iscnrm3llem2  49509  0setrec  50263