Theorem pw0 4766

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

Syntax hints:   = wceq 1540  {cab 2707   ⊆ wss 3905  ∅c0 4286  𝒫 cpw 4553  {csn 4579

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-dif 3908  df-ss 3922  df-nul 4287  df-pw 4555  df-sn 4580

This theorem is referenced by:  p0ex  5326  pwfi  9226  ackbij1lem14  10145  fin1a2lem12  10324  0tsk  10668  hashbc  14378  incexclem  15761  sn0topon  22901  sn0cld  22993  ust0  24123  made0  27805  uhgr0vb  29035  uhgr0  29036  esumnul  34014  rankeq1o  36144  ssoninhaus  36421  sge00  46358