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 4358	. . 3 ⊢ (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2	1	abbii 2832	. 2 ⊢ {𝑥 ∣ 𝑥 ⊆ ∅} = {𝑥 ∣ 𝑥 = ∅}
3		df-pw 4560	. 2 ⊢ 𝒫 ∅ = {𝑥 ∣ 𝑥 ⊆ ∅}
4		df-sn 4586	. 2 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅}
5	2, 3, 4	3eqtr4i 2798	1 ⊢ 𝒫 ∅ = {∅}

Syntax hints:   = wceq 1563  {cab 2743   ⊆ wss 3907  ∅c0 4288  𝒫 cpw 4558  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-dif 3910  df-ss 3924  df-nul 4289  df-pw 4560  df-sn 4586

This theorem is referenced by:  p0ex  5345  pwfi  9266  ackbij1lem14  10203  fin1a2lem12  10383  0tsk  10728  hashbc  14478  incexclem  15878  sn0topon  23112  sn0cld  23204  ust0  24334  made0  28010  uhgr0vb  29327  uhgr0  29328  vieta  33882  esumnul  34350  r11  35397  rankeq1o  36529  ssoninhaus  36816  sge00  46949