Theorem bj-snglss

Description: The singletonization of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-snglss	$$⊢snglA\subseteq 𝒫A$$

Proof

Step	Hyp	Ref	Expression
1		bj-elsngl	$$⊢x\in snglA\leftrightarrow \exists y\in Ax=\left\{y\right\}$$
2		df-rex	$$⊢\exists y\in Ax=\left\{y\right\}\leftrightarrow \exists y\left(y\in A\wedge x=\left\{y\right\}\right)$$
3		snssi	$$⊢y\in A\to \left\{y\right\}\subseteq A$$
4		sseq1	$$⊢x=\left\{y\right\}\to \left(x\subseteq A\leftrightarrow \left\{y\right\}\subseteq A\right)$$
5	4	biimparc	$$⊢\left(\left\{y\right\}\subseteq A\wedge x=\left\{y\right\}\right)\to x\subseteq A$$
6	3 5	sylan	$$⊢\left(y\in A\wedge x=\left\{y\right\}\right)\to x\subseteq A$$
7	6	eximi	$$⊢\exists y\left(y\in A\wedge x=\left\{y\right\}\right)\to \exists yx\subseteq A$$
8	2 7	sylbi	$$⊢\exists y\in Ax=\left\{y\right\}\to \exists yx\subseteq A$$
9	1 8	sylbi	$$⊢x\in snglA\to \exists yx\subseteq A$$
10		ax5e	$$⊢\exists yx\subseteq A\to x\subseteq A$$
11	9 10	syl	$$⊢x\in snglA\to x\subseteq A$$
12		velpw	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$
13	11 12	sylibr	$$⊢x\in snglA\to x\in 𝒫A$$
14	13	ssriv	$$⊢snglA\subseteq 𝒫A$$