Theorem ss0 4425

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3976  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-dif 3979  df-ss 3993  df-nul 4353

This theorem is referenced by:  sseq0  4426  0dif  4428  eq0rdvALT  4431  ssdisj  4483  disjpss  4484  dfopif  4894  iunxdif3  5118  fr0  5678  poirr2  6156  sofld  6218  f00  6803  fvmptopab  7504  tfindsg  7898  findsg  7937  frxp  8167  map0b  8941  sbthlem7  9155  ssfi  9240  phplem2OLD  9281  fi0  9489  cantnflem1  9758  rankeq0b  9929  grur1a  10888  ixxdisj  13422  icodisj  13536  ioodisj  13542  uzdisj  13657  nn0disj  13701  hashf1lem2  14505  swrd0  14706  xptrrel  15029  sumz  15770  sumss  15772  fsum2dlem  15818  prod1  15992  prodss  15995  fprodss  15996  fprod2dlem  16028  cntzval  19361  oppglsm  19684  efgval  19759  islss  20955  00lss  20962  mplsubglem  22042  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  24902  itg1addlem4  25753  itg1addlem4OLD  25754  uc1pval  26199  mon1pval  26201  pserulm  26483  vtxdun  29517  vtxdginducedm1  29579  difres  32622  imadifxp  32623  swrdrndisj  32924  cycpmco2f1  33117  erlval  33230  ssdifidllem  33449  ply1dg3rt0irred  33572  esumrnmpt2  34032  truae  34207  carsgclctunlem2  34284  acycgr0v  35116  prclisacycgr  35119  derangsn  35138  poimirlem3  37583  ismblfin  37621  pcl0N  39879  pcl0bN  39880  coeq0i  42709  eldioph2lem2  42717  eldioph4b  42767  oe0suclim  43239  ntrk2imkb  43999  ntrk0kbimka  44001  ssin0  44957  iccdifprioo  45434  sumnnodd  45551  sge0split  46330  iscnrm3llem2  48630  0setrec  48796