Theorem pw0 4738

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 4344	. . 3 ⊢ (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2	1	abbii 2885	. 2 ⊢ {𝑥 ∣ 𝑥 ⊆ ∅} = {𝑥 ∣ 𝑥 = ∅}
3		df-pw 4534	. 2 ⊢ 𝒫 ∅ = {𝑥 ∣ 𝑥 ⊆ ∅}
4		df-sn 4561	. 2 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅}
5	2, 3, 4	3eqtr4i 2853	1 ⊢ 𝒫 ∅ = {∅}

Syntax hints:   = wceq 1536  {cab 2798   ⊆ wss 3929  ∅c0 4284  𝒫 cpw 4532  {csn 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2799  df-cleq 2813  df-clel 2892  df-dif 3932  df-in 3936  df-ss 3945  df-nul 4285  df-pw 4534  df-sn 4561

This theorem is referenced by:  p0ex  5278  pwfi  8812  ackbij1lem14  9648  fin1a2lem12  9826  0tsk  10170  hashbc  13808  incexclem  15186  sn0topon  21601  sn0cld  21693  ust0  22823  uhgr0vb  26855  uhgr0  26856  esumnul  31328  rankeq1o  33653  ssoninhaus  33817  sge00  42732