Theorem ss0 3816

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 3815	. 2 |- ( A C_ (/) <-> A = (/) )
2	1	biimpi 194	1 |- ( A C_ (/) -> A = (/) )

Syntax hints:   -> wi 4   = wceq 1379   C_ wss 3476   (/)c0 3785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-dif 3479  df-in 3483  df-ss 3490  df-nul 3786

This theorem is referenced by:  sseq0  3817  abf  3819  eq0rdv  3820  ssdisj  3876  disjpss  3877  0dif  3898  dfopif  4210  fr0  4858  poirr2  5391  sofld  5455  f00  5767  tfindsg  6679  findsg  6711  frxp  6893  map0b  7457  sbthlem7  7633  phplem2  7697  fi0  7880  cantnflem1  8108  cantnflem1OLD  8131  rankeq0b  8278  grur1a  9197  ixxdisj  11544  icodisj  11645  ioodisj  11650  uzdisj  11751  nn0disj  11788  hashf1lem2  12471  swrd0  12621  sumz  13507  sumss  13509  fsum2dlem  13548  cntzval  16164  symgbas  16210  oppglsm  16468  efgval  16541  islss  17381  00lss  17388  mplsubglem  17892  mplsubglemOLD  17894  ntrcls0  19371  neindisj2  19418  hauscmplem  19700  fbdmn0  20098  fbncp  20103  opnfbas  20106  fbasfip  20132  fbunfip  20133  fgcl  20142  supfil  20159  ufinffr  20193  alexsubALTlem2  20311  metnrmlem3  21128  itg1addlem4  21869  uc1pval  22303  mon1pval  22305  pserulm  22579  vdgrun  24605  vdgrfiun  24606  difres  27158  imadifxp  27159  measunl  27855  truae  27883  derangsn  28282  prod1  28681  prodss  28684  fprodss  28685  fprod2dlem  28715  ismblfin  29660  coeq0i  30318  eldioph2lem2  30326  eldioph4b  30377  iccdifprioo  31148  sumnnodd  31200  pcl0N  34736  pcl0bN  34737  xptrrel  36803