Theorem pw0 4837

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

Step	Hyp	Ref	Expression
1		ss0b 4424	. . 3 ⊢ (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2	1	abbii 2812	. 2 ⊢ {𝑥 ∣ 𝑥 ⊆ ∅} = {𝑥 ∣ 𝑥 = ∅}
3		df-pw 4624	. 2 ⊢ 𝒫 ∅ = {𝑥 ∣ 𝑥 ⊆ ∅}
4		df-sn 4649	. 2 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅}
5	2, 3, 4	3eqtr4i 2778	1 ⊢ 𝒫 ∅ = {∅}

Syntax hints:   = wceq 1537  {cab 2717   ⊆ wss 3976  ∅c0 4352  𝒫 cpw 4622  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-dif 3979  df-ss 3993  df-nul 4353  df-pw 4624  df-sn 4649

This theorem is referenced by:  p0ex  5402  pwfi  9385  pwfiOLD  9417  ackbij1lem14  10301  fin1a2lem12  10480  0tsk  10824  hashbc  14502  incexclem  15884  sn0topon  23026  sn0cld  23119  ust0  24249  made0  27930  uhgr0vb  29107  uhgr0  29108  esumnul  34012  rankeq1o  36135  ssoninhaus  36414  sge00  46297