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	$⊢ 𝒫 \emptyset = \{\emptyset\}$

Proof

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