Theorem pw0 4779

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

Syntax hints:   = wceq 1570  {cab 2741   ⊆ wss 3906  ∅c0 4287  𝒫 cpw 4563  {csn 4590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-dif 3909  df-ss 3923  df-nul 4288  df-pw 4565  df-sn 4591

This theorem is referenced by:  p0ex  5357  pwfi  9279  ackbij1lem14  10216  fin1a2lem12  10396  0tsk  10741  hashbc  14492  incexclem  15892  sn0topon  23136  sn0cld  23228  ust0  24358  made0  28037  uhgr0vb  29403  uhgr0  29404  vieta  33951  esumnul  34419  r11  35468  rankeq1o  36644  ssoninhaus  36940  sge00  47073