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	$$⊢𝒫\varnothing =\left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		ss0b	$$⊢x\subseteq \varnothing \leftrightarrow x=\varnothing$$
2	1	abbii	$$⊢\left\{x|x\subseteq \varnothing \right\}=\left\{x|x=\varnothing \right\}$$
3		df-pw	$$⊢𝒫\varnothing =\left\{x|x\subseteq \varnothing \right\}$$
4		df-sn	$$⊢\left\{\varnothing \right\}=\left\{x|x=\varnothing \right\}$$
5	2 3 4	3eqtr4i	$$⊢𝒫\varnothing =\left\{\varnothing \right\}$$