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

Theorem ss0b 3759
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 3758 . . 3  |-  (/)  C_  A
2 eqss 3449 . . 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 1399    C_ wss 3406   (/)c0 3728
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-v 3053  df-dif 3409  df-in 3413  df-ss 3420  df-nul 3729
This theorem is referenced by:  ss0  3760  un00  3795  ssdisj  3809  pw0  4108  fnsuppeq0  6868  cnfcom2lem  8080  cnfcom2lemOLD  8088  card0  8274  kmlem5  8469  cf0  8566  fin1a2lem12  8726  mreexexlem3d  15076  efgval  16875  ppttop  19616  0nnei  19722  disjunsn  27617  isarchi  27913  filnetlem4  30405  pnonsingN  36109  osumcllem4N  36135
  Copyright terms: Public domain W3C validator