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

Theorem pw0 3841
Description: Compute the power set of the empty set. Theorem 89 of [Suppes] p. 47. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
Assertion
Ref Expression
pw0  |-  ~P (/)  =  { (/)
}

Proof of Theorem pw0
StepHypRef Expression
1 ss0b 3560 . . 3  |-  ( x 
C_  (/)  <->  x  =  (/) )
21abbii 2470 . 2  |-  { x  |  x  C_  (/) }  =  { x  |  x  =  (/) }
3 df-pw 3703 . 2  |-  ~P (/)  =  {
x  |  x  C_  (/)
}
4 df-sn 3722 . 2  |-  { (/) }  =  { x  |  x  =  (/) }
52, 3, 43eqtr4i 2388 1  |-  ~P (/)  =  { (/)
}
Colors of variables: wff set class
Syntax hints:    = wceq 1642   {cab 2344    C_ wss 3228   (/)c0 3531   ~Pcpw 3701   {csn 3716
This theorem is referenced by:  p0ex  4278  pwfi  7241  ackbij1lem14  7949  fin1a2lem12  8127  0tsk  8467  hashbc  11487  incexclem  12392  sn0topon  16841  sn0cld  16933  ust0  23523  esumnul  23709  rankeq1o  25360  ssoninhaus  25446  uhgra0v  27517  usgra0v  27546
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-dif 3231  df-in 3235  df-ss 3242  df-nul 3532  df-pw 3703  df-sn 3722
  Copyright terms: Public domain W3C validator