Theorem pw0 4783

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 4361	. . 3 ⊢ (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2	1	abbii 2833	. 2 ⊢ {𝑥 ∣ 𝑥 ⊆ ∅} = {𝑥 ∣ 𝑥 = ∅}
3		df-pw 4569	. 2 ⊢ 𝒫 ∅ = {𝑥 ∣ 𝑥 ⊆ ∅}
4		df-sn 4595	. 2 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅}
5	2, 3, 4	3eqtr4i 2799	1 ⊢ 𝒫 ∅ = {∅}

This proof depends on syntax axioms:   = wceq 1570  {cab 2744   ⊆ wss 3908  ∅c0 4289  𝒫 cpw 4567  {csn 4594

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-dif 3911  df-ss 3925  df-nul 4290  df-pw 4569  df-sn 4595

This theorem is used by:  p0ex  5360  pwfi  9288  ackbij1lem14  10234  fin1a2lem12  10413  0tsk  10758  hashbc  14510  incexclem  15916  sn0topon  23192  sn0cld  23284  ust0  24414  made0  28093  uhgr0vb  29459  uhgr0  29460  vieta  34001  esumnul  34469  r11  35512  rankeq1o  36684  ssoninhaus  37000  sge00  47131