Theorem ss0 3618

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

Syntax hints:   -> wi 4   = wceq 1649   C_ wss 3280   (/)c0 3588

This theorem is referenced by:  sseq0  3619  abf  3621  eq0rdv  3622  ssdisj  3637  disjpss  3638  0dif  3659  dfopif  3941  fr0  4521  tfindsg  4799  findsg  4831  poirr2  5217  sofld  5277  f00  5587  frxp  6415  map0b  7011  sbthlem7  7182  phplem2  7246  fi0  7383  cantnflem1  7601  rankeq0b  7742  grur1a  8650  ixxdisj  10887  icodisj  10978  ioodisj  10982  uzdisj  11074  hashf1lem2  11660  sumz  12471  sumss  12473  fsum2dlem  12509  symgbas  15050  cntzval  15075  oppglsm  15231  efgval  15304  islss  15966  00lss  15973  mplsubglem  16453  ntrcls0  17095  neindisj2  17142  hauscmplem  17423  fbdmn0  17819  fbncp  17824  opnfbas  17827  fbasfip  17853  fbunfip  17854  fgcl  17863  supfil  17880  ufinffr  17914  alexsubALTlem2  18032  metnrmlem3  18844  itg1addlem4  19544  mdeg0  19946  uc1pval  20015  mon1pval  20017  pserulm  20291  vdgrun  21625  vdgrfiun  21626  imadifxp  23991  measunl  24523  truae  24547  derangsn  24809  prod1  25223  prodss  25226  fprodss  25227  fprod2dlem  25257  ismblfin  26146  coeq0i  26701  eldioph2lem2  26709  eldioph4b  26762  pcl0N  30404  pcl0bN  30405

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-dif 3283  df-in 3287  df-ss 3294  df-nul 3589