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

Theorem ss0b 3497
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 3496 . . 3  |-  (/)  C_  A
2 eqss 3207 . . 3  |-  ( A  =  (/)  <->  ( A  C_  (/) 
/\  (/)  C_  A )
)
31, 2mpbiran2 885 . 2  |-  ( A  =  (/)  <->  A  C_  (/) )
43bicomi 193 1  |-  ( A 
C_  (/)  <->  A  =  (/) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1632    C_ wss 3165   (/)c0 3468
This theorem is referenced by:  ss0  3498  un00  3503  ssdisj  3517  pw0  3778  fnsuppeq0  5749  cnfcom2lem  7420  card0  7607  kmlem5  7796  cf0  7893  fin1a2lem12  8053  mreexexlem3d  13564  efgval  15042  ppttop  16760  0nnei  16865  sssu  25244  filnetlem4  26433  pnonsingN  30744  osumcllem4N  30770
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168  df-in 3172  df-ss 3179  df-nul 3469
  Copyright terms: Public domain W3C validator