Theorem ss0 4402

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3951  ∅c0 4333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-dif 3954  df-ss 3968  df-nul 4334

This theorem is referenced by:  sseq0  4403  0dif  4405  eq0rdvALT  4408  ssdisj  4460  disjpss  4461  dfopif  4870  iunxdif3  5095  fr0  5663  poirr2  6144  sofld  6207  f00  6790  fvmptopab  7487  tfindsg  7882  findsg  7919  frxp  8151  map0b  8923  sbthlem7  9129  ssfi  9213  phplem2OLD  9255  fi0  9460  cantnflem1  9729  rankeq0b  9900  grur1a  10859  ixxdisj  13402  icodisj  13516  ioodisj  13522  uzdisj  13637  nn0disj  13684  hashf1lem2  14495  swrd0  14696  xptrrel  15019  sumz  15758  sumss  15760  fsum2dlem  15806  prod1  15980  prodss  15983  fprodss  15984  fprod2dlem  16016  cntzval  19339  oppglsm  19660  efgval  19735  islss  20932  00lss  20939  mplsubglem  22019  ntrcls0  23084  neindisj2  23131  hauscmplem  23414  fbdmn0  23842  fbncp  23847  opnfbas  23850  fbasfip  23876  fbunfip  23877  fgcl  23886  supfil  23903  ufinffr  23937  alexsubALTlem2  24056  metnrmlem3  24883  itg1addlem4  25734  uc1pval  26179  mon1pval  26181  pserulm  26465  vtxdun  29499  vtxdginducedm1  29561  difres  32613  imadifxp  32614  swrdrndisj  32942  cycpmco2f1  33144  erlval  33262  ssdifidllem  33484  ply1dg3rt0irred  33607  esumrnmpt2  34069  truae  34244  carsgclctunlem2  34321  acycgr0v  35153  prclisacycgr  35156  derangsn  35175  poimirlem3  37630  ismblfin  37668  pcl0N  39924  pcl0bN  39925  coeq0i  42764  eldioph2lem2  42772  eldioph4b  42822  oe0suclim  43290  ntrk2imkb  44050  ntrk0kbimka  44052  ssin0  45060  iccdifprioo  45529  sumnnodd  45645  sge0split  46424  iscnrm3llem2  48847  0setrec  49223