Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ss0b 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 3518 . . 3
31, 2mpbiran2 919 . 2
43bicomi 202 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  =wceq 1395  C_wss 3475   c0 3784 This theorem is referenced by:  ss0  3816  un00  3862  ssdisj  3876  pw0  4177  fnsuppeq0OLD  6132  fnsuppeq0  6947  cnfcom2lem  8166  cnfcom2lemOLD  8174  card0  8360  kmlem5  8555  cf0  8652  fin1a2lem12  8812  mreexexlem3d  15043  efgval  16735  ppttop  19508  0nnei  19613  disjunsn  27453  isarchi  27726  filnetlem4  30199  pnonsingN  35657  osumcllem4N  35683 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489  df-nul 3785
 Copyright terms: Public domain W3C validator