Theorem pw0 4767

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 4352	. . 3 ⊢ (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2	1	abbii 2828	. 2 ⊢ {𝑥 ∣ 𝑥 ⊆ ∅} = {𝑥 ∣ 𝑥 = ∅}
3		df-pw 4554	. 2 ⊢ 𝒫 ∅ = {𝑥 ∣ 𝑥 ⊆ ∅}
4		df-sn 4580	. 2 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅}
5	2, 3, 4	3eqtr4i 2794	1 ⊢ 𝒫 ∅ = {∅}

Syntax hints:   = wceq 1559  {cab 2739   ⊆ wss 3902  ∅c0 4283  𝒫 cpw 4552  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-dif 3905  df-ss 3919  df-nul 4284  df-pw 4554  df-sn 4580

This theorem is referenced by:  p0ex  5338  pwfi  9256  ackbij1lem14  10181  fin1a2lem12  10361  0tsk  10706  hashbc  14459  incexclem  15856  sn0topon  23045  sn0cld  23137  ust0  24267  made0  27943  uhgr0vb  29229  uhgr0  29230  vieta  33837  esumnul  34305  r11  35350  rankeq1o  36481  ssoninhaus  36768  sge00  46910