Theorem pw0 4711

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 4298	. . 3 ⊢ (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2	1	abbii 2801	. 2 ⊢ {𝑥 ∣ 𝑥 ⊆ ∅} = {𝑥 ∣ 𝑥 = ∅}
3		df-pw 4501	. 2 ⊢ 𝒫 ∅ = {𝑥 ∣ 𝑥 ⊆ ∅}
4		df-sn 4528	. 2 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅}
5	2, 3, 4	3eqtr4i 2769	1 ⊢ 𝒫 ∅ = {∅}

Syntax hints:   = wceq 1543  {cab 2714   ⊆ wss 3853  ∅c0 4223  𝒫 cpw 4499  {csn 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-dif 3856  df-in 3860  df-ss 3870  df-nul 4224  df-pw 4501  df-sn 4528

This theorem is referenced by:  p0ex  5262  pwfi  8833  pwfiOLD  8949  ackbij1lem14  9812  fin1a2lem12  9990  0tsk  10334  hashbc  13982  incexclem  15363  sn0topon  21849  sn0cld  21941  ust0  23071  uhgr0vb  27117  uhgr0  27118  esumnul  31682  made0  33743  rankeq1o  34159  ssoninhaus  34323  sge00  43532