Theorem pw0 4770

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

Syntax hints:   = wceq 1542  {cab 2715   ⊆ wss 3903  ∅c0 4287  𝒫 cpw 4556  {csn 4582

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 3906  df-ss 3920  df-nul 4288  df-pw 4558  df-sn 4583

This theorem is referenced by:  p0ex  5331  pwfi  9231  ackbij1lem14  10154  fin1a2lem12  10333  0tsk  10678  hashbc  14388  incexclem  15771  sn0topon  22954  sn0cld  23046  ust0  24176  made0  27871  uhgr0vb  29157  uhgr0  29158  vieta  33756  esumnul  34225  r11  35269  rankeq1o  36384  ssoninhaus  36661  sge00  46728