This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pw0

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)

		Ref	Expression
	Assertion	pw0	⊢ 𝒫 ∅ = { ∅ }

Proof

Step	Hyp	Ref	Expression
1		ss0b	⊢ ( 𝑥 ⊆ ∅ ↔ 𝑥 = ∅ )
2	1	abbii	⊢ { 𝑥 ∣ 𝑥 ⊆ ∅ } = { 𝑥 ∣ 𝑥 = ∅ }
3		df-pw	⊢ 𝒫 ∅ = { 𝑥 ∣ 𝑥 ⊆ ∅ }
4		df-sn	⊢ { ∅ } = { 𝑥 ∣ 𝑥 = ∅ }
5	2 3 4	3eqtr4i	⊢ 𝒫 ∅ = { ∅ }