Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ss0b Structured version   Unicode version

Theorem ss0b 3815
 Description: Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23 and its converse. (Contributed by NM, 17-Sep-2003.)
Assertion
Ref Expression
ss0b

Proof of Theorem ss0b
StepHypRef Expression
1 0ss 3814 . . 3
2 eqss 3519 . . 3
31, 2mpbiran2 917 . 2
43bicomi 202 1
 Colors of variables: wff setvar class Syntax hints:   wb 184   wceq 1379   wss 3476  c0 3785 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-dif 3479  df-in 3483  df-ss 3490  df-nul 3786 This theorem is referenced by:  ss0  3816  un00  3862  ssdisj  3876  pw0  4174  fnsuppeq0OLD  6120  fnsuppeq0  6925  cnfcom2lem  8141  cnfcom2lemOLD  8149  card0  8335  kmlem5  8530  cf0  8627  fin1a2lem12  8787  mreexexlem3d  14897  efgval  16531  ppttop  19274  0nnei  19379  disjunsn  27126  isarchi  27388  filnetlem4  29802  pnonsingN  34729  osumcllem4N  34755
 Copyright terms: Public domain W3C validator