Theorem ss0 3738

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

Syntax hints:   -> wi 4   = wceq 1437   C_ wss 3379   (/)c0 3704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-dif 3382  df-in 3386  df-ss 3393  df-nul 3705

This theorem is referenced by:  sseq0  3739  abf  3741  eq0rdv  3742  ssdisj  3787  disjpss  3788  0dif  3811  dfopif  4127  fr0  4775  poirr2  5186  sofld  5246  f00  5725  tfindsg  6645  findsg  6678  frxp  6861  map0b  7465  sbthlem7  7641  phplem2  7705  fi0  7887  cantnflem1  8146  rankeq0b  8283  grur1a  9195  ixxdisj  11601  icodisj  11708  ioodisj  11713  uzdisj  11818  nn0disj  11858  hashf1lem2  12567  swrd0  12736  xptrrel  12988  sumz  13731  sumss  13733  fsum2dlem  13774  prod1  13941  prodss  13944  fprodss  13945  fprod2dlem  13977  cntzval  16918  symgbas  16964  oppglsm  17237  efgval  17310  islss  18101  00lss  18108  mplsubglem  18601  ntrcls0  20034  neindisj2  20081  hauscmplem  20363  fbdmn0  20791  fbncp  20796  opnfbas  20799  fbasfip  20825  fbunfip  20826  fgcl  20835  supfil  20852  ufinffr  20886  alexsubALTlem2  21005  metnrmlem3  21820  metnrmlem3OLD  21835  itg1addlem4  22599  uc1pval  23032  mon1pval  23034  pserulm  23319  vdgrun  25571  vdgrfiun  25572  iunxdif3  28121  difres  28157  imadifxp  28158  esumrnmpt2  28841  truae  29018  carsgclctunlem2  29103  derangsn  29845  poimirlem3  31850  ismblfin  31888  pcl0N  33399  pcl0bN  33400  coeq0i  35507  eldioph2lem2  35515  eldioph4b  35566  ssin0  37311  iccdifprioo  37509  sumnnodd  37593  sge0split  38102