Theorem ss0 3668

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

Syntax hints:   -> wi 4   = wceq 1369   C_ wss 3328   (/)c0 3637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2974  df-dif 3331  df-in 3335  df-ss 3342  df-nul 3638

This theorem is referenced by:  sseq0  3669  abf  3671  eq0rdv  3672  ssdisj  3728  disjpss  3729  0dif  3750  dfopif  4056  fr0  4699  poirr2  5222  sofld  5286  f00  5593  tfindsg  6471  findsg  6503  frxp  6682  map0b  7251  sbthlem7  7427  phplem2  7491  fi0  7670  cantnflem1  7897  cantnflem1OLD  7920  rankeq0b  8067  grur1a  8986  ixxdisj  11315  icodisj  11410  ioodisj  11415  uzdisj  11531  hashf1lem2  12209  swrd0  12327  sumz  13199  sumss  13201  fsum2dlem  13237  cntzval  15839  symgbas  15885  oppglsm  16141  efgval  16214  islss  17016  00lss  17023  mplsubglem  17510  mplsubglemOLD  17512  ntrcls0  18680  neindisj2  18727  hauscmplem  19009  fbdmn0  19407  fbncp  19412  opnfbas  19415  fbasfip  19441  fbunfip  19442  fgcl  19451  supfil  19468  ufinffr  19502  alexsubALTlem2  19620  metnrmlem3  20437  itg1addlem4  21177  uc1pval  21611  mon1pval  21613  pserulm  21887  vdgrun  23571  vdgrfiun  23572  imadifxp  25939  measunl  26630  truae  26659  derangsn  27058  prod1  27457  prodss  27460  fprodss  27461  fprod2dlem  27491  ismblfin  28432  coeq0i  29091  eldioph2lem2  29099  eldioph4b  29150  pcl0N  33566  pcl0bN  33567