Theorem pw0 4755

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 4341	. . 3 ⊢ (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2	1	abbii 2803	. 2 ⊢ {𝑥 ∣ 𝑥 ⊆ ∅} = {𝑥 ∣ 𝑥 = ∅}
3		df-pw 4543	. 2 ⊢ 𝒫 ∅ = {𝑥 ∣ 𝑥 ⊆ ∅}
4		df-sn 4568	. 2 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅}
5	2, 3, 4	3eqtr4i 2769	1 ⊢ 𝒫 ∅ = {∅}

Syntax hints:   = wceq 1542  {cab 2714   ⊆ wss 3889  ∅c0 4273  𝒫 cpw 4541  {csn 4567

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-dif 3892  df-ss 3906  df-nul 4274  df-pw 4543  df-sn 4568

This theorem is referenced by:  p0ex  5326  pwfi  9229  ackbij1lem14  10154  fin1a2lem12  10333  0tsk  10678  hashbc  14415  incexclem  15801  sn0topon  22963  sn0cld  23055  ust0  24185  made0  27855  uhgr0vb  29141  uhgr0  29142  vieta  33724  esumnul  34192  r11  35237  rankeq1o  36353  ssoninhaus  36630  sge00  46804