Theorem pwsn

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

	Ref	Expression
Assertion	pwsn	$$⊢𝒫\left\{A\right\}=\left\{\varnothing ,\left\{A\right\}\right\}$$

Proof

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