MPE Home 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  |-  ( A 
C_  (/)  <->  A  =  (/) )

Proof of Theorem ss0b
StepHypRef Expression
1 0ss 3814 . . 3  |-  (/)  C_  A
2 eqss 3519 . . 3  |-  ( A  =  (/)  <->  ( A  C_  (/) 
/\  (/)  C_  A )
)
31, 2mpbiran2 917 . 2  |-  ( A  =  (/)  <->  A  C_  (/) )
43bicomi 202 1  |-  ( A 
C_  (/)  <->  A  =  (/) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1379    C_ 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