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

Theorem pw0 4705
 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 𝒫 ∅ = {∅}

Proof of Theorem pw0
StepHypRef Expression
1 ss0b 4305 . . 3 (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
21abbii 2863 . 2 {𝑥𝑥 ⊆ ∅} = {𝑥𝑥 = ∅}
3 df-pw 4499 . 2 𝒫 ∅ = {𝑥𝑥 ⊆ ∅}
4 df-sn 4526 . 2 {∅} = {𝑥𝑥 = ∅}
52, 3, 43eqtr4i 2831 1 𝒫 ∅ = {∅}
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538  {cab 2776   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497  {csn 4525 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898  df-nul 4244  df-pw 4499  df-sn 4526 This theorem is referenced by:  p0ex  5250  pwfi  8803  ackbij1lem14  9644  fin1a2lem12  9822  0tsk  10166  hashbc  13807  incexclem  15183  sn0topon  21603  sn0cld  21695  ust0  22825  uhgr0vb  26865  uhgr0  26866  esumnul  31417  rankeq1o  33745  ssoninhaus  33909  sge00  43013
 Copyright terms: Public domain W3C validator