Theorem ss0 3802

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

Syntax hints:   -> wi 4   = wceq 1383   C_ wss 3461   (/)c0 3770

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-dif 3464  df-in 3468  df-ss 3475  df-nul 3771

This theorem is referenced by:  sseq0  3803  abf  3805  eq0rdv  3806  ssdisj  3862  disjpss  3863  0dif  3885  dfopif  4199  fr0  4848  poirr2  5381  sofld  5445  f00  5757  tfindsg  6680  findsg  6712  frxp  6895  map0b  7459  sbthlem7  7635  phplem2  7699  fi0  7882  cantnflem1  8111  cantnflem1OLD  8134  rankeq0b  8281  grur1a  9200  ixxdisj  11554  icodisj  11655  ioodisj  11660  uzdisj  11761  nn0disj  11801  hashf1lem2  12486  swrd0  12639  sumz  13525  sumss  13527  fsum2dlem  13566  prod1  13732  prodss  13735  fprodss  13736  fprod2dlem  13765  cntzval  16337  symgbas  16383  oppglsm  16640  efgval  16713  islss  17559  00lss  17566  mplsubglem  18071  mplsubglemOLD  18073  ntrcls0  19554  neindisj2  19601  hauscmplem  19883  fbdmn0  20312  fbncp  20317  opnfbas  20320  fbasfip  20346  fbunfip  20347  fgcl  20356  supfil  20373  ufinffr  20407  alexsubALTlem2  20525  metnrmlem3  21342  itg1addlem4  22083  uc1pval  22517  mon1pval  22519  pserulm  22793  vdgrun  24877  vdgrfiun  24878  difres  27433  imadifxp  27434  truae  28192  derangsn  28591  ismblfin  30030  coeq0i  30661  eldioph2lem2  30669  eldioph4b  30720  iccdifprioo  31492  sumnnodd  31544  pcl0N  35386  pcl0bN  35387  xptrrel  37468