Theorem pw0 4751

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 4337	. . 3 ⊢ (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2	1	abbii 2810	. 2 ⊢ {𝑥 ∣ 𝑥 ⊆ ∅} = {𝑥 ∣ 𝑥 = ∅}
3		df-pw 4541	. 2 ⊢ 𝒫 ∅ = {𝑥 ∣ 𝑥 ⊆ ∅}
4		df-sn 4568	. 2 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅}
5	2, 3, 4	3eqtr4i 2778	1 ⊢ 𝒫 ∅ = {∅}

Syntax hints:   = wceq 1542  {cab 2717   ⊆ wss 3892  ∅c0 4262  𝒫 cpw 4539  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-dif 3895  df-in 3899  df-ss 3909  df-nul 4263  df-pw 4541  df-sn 4568

This theorem is referenced by:  p0ex  5311  pwfi  8943  pwfiOLD  9092  ackbij1lem14  9990  fin1a2lem12  10168  0tsk  10512  hashbc  14163  incexclem  15546  sn0topon  22146  sn0cld  22239  ust0  23369  uhgr0vb  27440  uhgr0  27441  esumnul  32012  made0  34053  rankeq1o  34469  ssoninhaus  34633  sge00  43885