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

Theorem ss0b 3484
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 3483 . . 3  |-  (/)  C_  A
2 eqss 3194 . . 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 1623    C_ wss 3152   (/)c0 3455
This theorem is referenced by:  ss0  3485  un00  3490  ssdisj  3504  pw0  3762  fnsuppeq0  5733  cnfcom2lem  7404  card0  7591  kmlem5  7780  cf0  7877  fin1a2lem12  8037  mreexexlem3d  13548  efgval  15026  ppttop  16744  0nnei  16849  sssu  25141  filnetlem4  26330  pnonsingN  30122  osumcllem4N  30148
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-in 3159  df-ss 3166  df-nul 3456
  Copyright terms: Public domain W3C validator