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

Metamath Proof Explorer

Theorem pwsn

Description: The power set of a singleton. (Contributed by NM, 5-Jun-2006)

		Ref	Expression
	Assertion	pwsn	$⊢ 𝒫 \{A\} = \{\emptyset, \{A\}\}$

Step	Hyp	Ref	Expression
1		sssn	$⊢ x \subseteq \{A\} \leftrightarrow (x = \emptyset \lor x = \{A\})$
2	1	abbii	$⊢ \{x \| x \subseteq \{A\}\} = \{x \| (x = \emptyset \lor x = \{A\})\}$
3		df-pw	$⊢ 𝒫 \{A\} = \{x \| x \subseteq \{A\}\}$
4		dfpr2	$⊢ \{\emptyset, \{A\}\} = \{x \| (x = \emptyset \lor x = \{A\})\}$
5	2 3 4	3eqtr4i	$⊢ 𝒫 \{A\} = \{\emptyset, \{A\}\}$