Theorem pw0 4776

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 4354	. . 3 ⊢ (𝑥 ⊆ ∅ ↔ 𝑥 = ∅)
2	1	abbii 2829	. 2 ⊢ {𝑥 ∣ 𝑥 ⊆ ∅} = {𝑥 ∣ 𝑥 = ∅}
3		df-pw 4562	. 2 ⊢ 𝒫 ∅ = {𝑥 ∣ 𝑥 ⊆ ∅}
4		df-sn 4588	. 2 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅}
5	2, 3, 4	3eqtr4i 2795	1 ⊢ 𝒫 ∅ = {∅}

This proof depends on syntax axioms:   = wceq 1570  {cab 2740   ⊆ wss 3902  ∅c0 4282  𝒫 cpw 4560  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-dif 3905  df-ss 3919  df-nul 4283  df-pw 4562  df-sn 4588

This theorem is used by:  p0ex  5353  pwfi  9292  ackbij1lem14  10238  fin1a2lem12  10417  0tsk  10768  hashbc  14522  incexclem  15929  sn0topon  23229  sn0cld  23321  ust0  24452  made0  28136  uhgr0vb  29537  uhgr0  29538  vieta  34098  esumnul  34566  r11  35609  rankeq1o  36759  ssoninhaus  37075  sge00  47212