Theorem pw0 4764

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 2798	. 2 ⊢ {𝑥 ∣ 𝑥 ⊆ ∅} = {𝑥 ∣ 𝑥 = ∅}
3		df-pw 4552	. 2 ⊢ 𝒫 ∅ = {𝑥 ∣ 𝑥 ⊆ ∅}
4		df-sn 4577	. 2 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅}
5	2, 3, 4	3eqtr4i 2764	1 ⊢ 𝒫 ∅ = {∅}

Syntax hints:   = wceq 1541  {cab 2709   ⊆ wss 3902  ∅c0 4283  𝒫 cpw 4550  {csn 4576

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-dif 3905  df-ss 3919  df-nul 4284  df-pw 4552  df-sn 4577

This theorem is referenced by:  p0ex  5322  pwfi  9203  ackbij1lem14  10120  fin1a2lem12  10299  0tsk  10643  hashbc  14357  incexclem  15740  sn0topon  22911  sn0cld  23003  ust0  24133  made0  27816  uhgr0vb  29048  uhgr0  29049  esumnul  34056  rankeq1o  36204  ssoninhaus  36481  sge00  46413