Theorem pw0 4750

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 4336	. . 3 ⊢ (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2	1	abbii 2807	. 2 ⊢ {𝑥 ∣ 𝑥 ⊆ ∅} = {𝑥 ∣ 𝑥 = ∅}
3		df-pw 4538	. 2 ⊢ 𝒫 ∅ = {𝑥 ∣ 𝑥 ⊆ ∅}
4		df-sn 4563	. 2 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅}
5	2, 3, 4	3eqtr4i 2773	1 ⊢ 𝒫 ∅ = {∅}

Syntax hints:   = wceq 1547  {cab 2718   ⊆ wss 3890  ∅c0 4268  𝒫 cpw 4536  {csn 4562

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-dif 3893  df-ss 3907  df-nul 4269  df-pw 4538  df-sn 4563

This theorem is referenced by:  p0ex  5320  pwfi  9226  ackbij1lem14  10152  fin1a2lem12  10331  0tsk  10676  hashbc  14413  incexclem  15799  sn0topon  22988  sn0cld  23080  ust0  24210  made0  27880  uhgr0vb  29166  uhgr0  29167  vieta  33771  esumnul  34239  r11  35282  rankeq1o  36406  ssoninhaus  36683  sge00  46826