Theorem snsspw

Description: The singleton of a class is a subset of its power class. (Contributed by NM, 21-Jun-1993)

	Ref	Expression
Assertion	snsspw	$$⊢\left\{A\right\}\subseteq 𝒫A$$

Proof

Step	Hyp	Ref	Expression
1		eqimss	$$⊢x=A\to x\subseteq A$$
2		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
3		velpw	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$
4	1 2 3	3imtr4i	$$⊢x\in \left\{A\right\}\to x\in 𝒫A$$
5	4	ssriv	$$⊢\left\{A\right\}\subseteq 𝒫A$$