Theorem pw0 4773

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 2828	. 2 ⊢ {𝑥 ∣ 𝑥 ⊆ ∅} = {𝑥 ∣ 𝑥 = ∅}
3		df-pw 4559	. 2 ⊢ 𝒫 ∅ = {𝑥 ∣ 𝑥 ⊆ ∅}
4		df-sn 4585	. 2 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅}
5	2, 3, 4	3eqtr4i 2794	1 ⊢ 𝒫 ∅ = {∅}

This proof depends on syntax axioms:   = wceq 1570  {cab 2739   ⊆ wss 3899  ∅c0 4279  𝒫 cpw 4557  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-dif 3902  df-ss 3916  df-nul 4280  df-pw 4559  df-sn 4585

This theorem is used by:  p0ex  5346  pwfi  9294  ackbij1lem14  10291  fin1a2lem12  10470  0tsk  10821  hashbc  14578  incexclem  15985  sn0topon  23296  sn0cld  23388  ust0  24519  made0  28231  uhgr0vb  29632  uhgr0  29633  vieta  34194  esumnul  34662  r11  35704  rankeq1o  36902  ssoninhaus  37206  sge00  47330