Theorem ss0 2902

Description: Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23.

Assertion

Ref	Expression
ss0	|- (A C_ (/) -> A = (/))

Proof of Theorem ss0

Step	Hyp	Ref	Expression
1		ss0b 2901	. 2 |- (A C_ (/) <-> A = (/))
2	1	biimpi 168	1 |- (A C_ (/) -> A = (/))

Syntax hints:   -> wi 3   = wceq 1298   C_ wss 2593  (/)c0 2875

This theorem is referenced by:  sseq0 2903  abf 2906  npss0OLD 2912  ssdisj 2923  disjpss 2924  0dif 2944  fr0 3636  tfindsg 3944  findsg 3980  unixp0 4423  f00 4601  tz6.12-2 4696  map0b 5402  sbthlem7 5516  mapdom2lem 5587  phplem2 5603  rankeq0 5807  infxpidmlem11 8831  ntrcls0 8983  fsubbas 10281  fgfil 10290  frxp 13951  fgsb 14921  fgsb2 14925  clindistop 14962  singempcon 14965  hscptsscld 15434  compfipin0 15436  alexsublem2 15438  isnrm2 15552  opnfbas 15557  supfil 15560  ufinffr 15578  fcluscf 15612  fcluscomp 15621

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-dif 2597  df-in 2603  df-ss 2605  df-nul 2876

Copyright terms: Public domain