Theorem pw0 4756

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 4342	. . 3 ⊢ (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2	1	abbii 2804	. 2 ⊢ {𝑥 ∣ 𝑥 ⊆ ∅} = {𝑥 ∣ 𝑥 = ∅}
3		df-pw 4544	. 2 ⊢ 𝒫 ∅ = {𝑥 ∣ 𝑥 ⊆ ∅}
4		df-sn 4569	. 2 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅}
5	2, 3, 4	3eqtr4i 2770	1 ⊢ 𝒫 ∅ = {∅}

Syntax hints:   = wceq 1542  {cab 2715   ⊆ wss 3890  ∅c0 4274  𝒫 cpw 4542  {csn 4568

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-dif 3893  df-ss 3907  df-nul 4275  df-pw 4544  df-sn 4569

This theorem is referenced by:  p0ex  5321  pwfi  9222  ackbij1lem14  10145  fin1a2lem12  10324  0tsk  10669  hashbc  14406  incexclem  15792  sn0topon  22973  sn0cld  23065  ust0  24195  made0  27869  uhgr0vb  29155  uhgr0  29156  vieta  33739  esumnul  34208  r11  35253  rankeq1o  36369  ssoninhaus  36646  sge00  46822