Theorem pw0 4745

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

Syntax hints:   = wceq 1537  {cab 2799   ⊆ wss 3936  ∅c0 4291  𝒫 cpw 4539  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-dif 3939  df-in 3943  df-ss 3952  df-nul 4292  df-pw 4541  df-sn 4568

This theorem is referenced by:  p0ex  5285  pwfi  8819  ackbij1lem14  9655  fin1a2lem12  9833  0tsk  10177  hashbc  13812  incexclem  15191  sn0topon  21606  sn0cld  21698  ust0  22828  uhgr0vb  26857  uhgr0  26858  esumnul  31307  rankeq1o  33632  ssoninhaus  33796  sge00  42678