Theorem pw0 4777

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 4362	. . 3 ⊢ (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2	1	abbii 2801	. 2 ⊢ {𝑥 ∣ 𝑥 ⊆ ∅} = {𝑥 ∣ 𝑥 = ∅}
3		df-pw 4567	. 2 ⊢ 𝒫 ∅ = {𝑥 ∣ 𝑥 ⊆ ∅}
4		df-sn 4592	. 2 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅}
5	2, 3, 4	3eqtr4i 2769	1 ⊢ 𝒫 ∅ = {∅}

Syntax hints:   = wceq 1541  {cab 2708   ⊆ wss 3913  ∅c0 4287  𝒫 cpw 4565  {csn 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-dif 3916  df-in 3920  df-ss 3930  df-nul 4288  df-pw 4567  df-sn 4592

This theorem is referenced by:  p0ex  5344  pwfi  9129  pwfiOLD  9298  ackbij1lem14  10178  fin1a2lem12  10356  0tsk  10700  hashbc  14362  incexclem  15732  sn0topon  22385  sn0cld  22478  ust0  23608  made0  27246  uhgr0vb  28086  uhgr0  28087  esumnul  32736  rankeq1o  34832  ssoninhaus  34996  sge00  44737