Theorem ss0 3776

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	|- ( A C_ (/) -> A = (/) )

Proof of Theorem ss0

Step	Hyp	Ref	Expression
1		ss0b 3775	. 2 |- ( A C_ (/) <-> A = (/) )
2	1	biimpi 199	1 |- ( A C_ (/) -> A = (/) )

Syntax hints:   -> wi 4   = wceq 1454   C_ wss 3415   (/)c0 3742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-dif 3418  df-in 3422  df-ss 3429  df-nul 3743

This theorem is referenced by:  sseq0  3777  abf  3779  eq0rdv  3780  ssdisj  3825  disjpss  3826  0dif  3849  dfopif  4176  fr0  4831  poirr2  5242  sofld  5302  f00  5787  tfindsg  6713  findsg  6746  frxp  6932  map0b  7535  sbthlem7  7713  phplem2  7777  fi0  7959  cantnflem1  8219  rankeq0b  8356  grur1a  9269  ixxdisj  11678  icodisj  11785  ioodisj  11790  uzdisj  11895  nn0disj  11936  hashf1lem2  12651  swrd0  12826  xptrrel  13092  sumz  13836  sumss  13838  fsum2dlem  13879  prod1  14046  prodss  14049  fprodss  14050  fprod2dlem  14082  cntzval  17023  symgbas  17069  oppglsm  17342  efgval  17415  islss  18206  00lss  18213  mplsubglem  18706  ntrcls0  20140  neindisj2  20187  hauscmplem  20469  fbdmn0  20897  fbncp  20902  opnfbas  20905  fbasfip  20931  fbunfip  20932  fgcl  20941  supfil  20958  ufinffr  20992  alexsubALTlem2  21111  metnrmlem3  21926  metnrmlem3OLD  21941  itg1addlem4  22705  uc1pval  23138  mon1pval  23140  pserulm  23425  vdgrun  25677  vdgrfiun  25678  iunxdif3  28223  difres  28259  imadifxp  28260  esumrnmpt2  28937  truae  29114  carsgclctunlem2  29199  derangsn  29941  poimirlem3  31987  ismblfin  32025  pcl0N  33531  pcl0bN  33532  coeq0i  35639  eldioph2lem2  35647  eldioph4b  35698  ssin0  37432  iccdifprioo  37654  sumnnodd  37747  sge0split  38288  vtxduhgrun  39587