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

Theorem ss0b 3486
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 3485 . . 3  |-  (/)  C_  A
2 eqss 3196 . . 3  |-  ( A  =  (/)  <->  ( A  C_  (/) 
/\  (/)  C_  A )
)
31, 2mpbiran2 887 . 2  |-  ( A  =  (/)  <->  A  C_  (/) )
43bicomi 195 1  |-  ( A 
C_  (/)  <->  A  =  (/) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    = wceq 1624    C_ wss 3154   (/)c0 3457
This theorem is referenced by:  ss0  3487  un00  3492  ssdisj  3506  pw0  3764  fnsuppeq0  5695  cnfcom2lem  7400  card0  7587  kmlem5  7776  cf0  7873  fin1a2lem12  8033  mreexexlem3d  13543  efgval  15021  ppttop  16739  0nnei  16844  sssu  24541  filnetlem4  25730  pnonsingN  29390  osumcllem4N  29416
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-dif 3157  df-in 3161  df-ss 3168  df-nul 3458
  Copyright terms: Public domain W3C validator