Theorem ss0 3665

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

Syntax hints:   -> wi 4   = wceq 1364   C_ wss 3325   (/)c0 3634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-dif 3328  df-in 3332  df-ss 3339  df-nul 3635

This theorem is referenced by:  sseq0  3666  abf  3668  eq0rdv  3669  ssdisj  3725  disjpss  3726  0dif  3747  dfopif  4053  fr0  4695  poirr2  5219  sofld  5283  f00  5590  tfindsg  6470  findsg  6502  frxp  6681  map0b  7247  sbthlem7  7423  phplem2  7487  fi0  7666  cantnflem1  7893  cantnflem1OLD  7916  rankeq0b  8063  grur1a  8982  ixxdisj  11311  icodisj  11406  ioodisj  11411  uzdisj  11527  hashf1lem2  12205  swrd0  12323  sumz  13195  sumss  13197  fsum2dlem  13233  cntzval  15832  symgbas  15878  oppglsm  16134  efgval  16207  islss  16994  00lss  17001  mplsubglem  17500  mplsubglemOLD  17502  ntrcls0  18580  neindisj2  18627  hauscmplem  18909  fbdmn0  19307  fbncp  19312  opnfbas  19315  fbasfip  19341  fbunfip  19342  fgcl  19351  supfil  19368  ufinffr  19402  alexsubALTlem2  19520  metnrmlem3  20337  itg1addlem4  21077  uc1pval  21554  mon1pval  21556  pserulm  21830  vdgrun  23490  vdgrfiun  23491  imadifxp  25858  measunl  26550  truae  26579  derangsn  26972  prod1  27370  prodss  27373  fprodss  27374  fprod2dlem  27404  ismblfin  28341  coeq0i  29000  eldioph2lem2  29008  eldioph4b  29059  pcl0N  33254  pcl0bN  33255