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

Theorem pw0 4131
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 3778 . . 3  |-  ( x 
C_  (/)  <->  x  =  (/) )
21abbii 2588 . 2  |-  { x  |  x  C_  (/) }  =  { x  |  x  =  (/) }
3 df-pw 3973 . 2  |-  ~P (/)  =  {
x  |  x  C_  (/)
}
4 df-sn 3989 . 2  |-  { (/) }  =  { x  |  x  =  (/) }
52, 3, 43eqtr4i 2493 1  |-  ~P (/)  =  { (/)
}
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370   {cab 2439    C_ wss 3439   (/)c0 3748   ~Pcpw 3971   {csn 3988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-dif 3442  df-in 3446  df-ss 3453  df-nul 3749  df-pw 3973  df-sn 3989
This theorem is referenced by:  p0ex  4590  pwfi  7720  ackbij1lem14  8516  fin1a2lem12  8694  0tsk  9036  hashbc  12327  incexclem  13420  sn0topon  18737  sn0cld  18829  ust0  19929  uhgra0v  23416  usgra0v  23462  esumnul  26667  rankeq1o  28373  ssoninhaus  28458
  Copyright terms: Public domain W3C validator