Theorem pw0 4829

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 4350	. . 3 ⊢ (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2	1	abbii 2827	. 2 ⊢ {𝑥 ∣ 𝑥 ⊆ ∅} = {𝑥 ∣ 𝑥 = ∅}
3		df-pw 4558	. 2 ⊢ 𝒫 ∅ = {𝑥 ∣ 𝑥 ⊆ ∅}
4		df-sn 4585	. 2 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅}
5	2, 3, 4	3eqtr4i 2793	1 ⊢ 𝒫 ∅ = {∅}

This proof depends on syntax axioms:   = wceq 1569  {cab 2738   ⊆ wss 3895  ∅c0 4278  𝒫 cpw 4556  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-dif 4047  df-nul 4279  df-pw 4558  df-sn 4585

This theorem is used by:  p0ex  5345  pwfi  9314  ackbij1lem14  10314  fin1a2lem12  10493  0tsk  10844  hashbc  14602  incexclem  16011  sn0topon  23322  sn0cld  23414  ust0  24545  made0  28255  uhgr0vb  29656  uhgr0  29657  vieta  34259  esumnul  34727  r11  35778  rankeq1o  37025  ssoninhaus  37329  sge00  47480