Theorem sels

Description: If a class is a set, then it is a member of a set. (Contributed by BJ, 3-Apr-2019)

	Ref	Expression
Assertion	sels	$$⊢A\in V\to \exists xA\in x$$

Proof

Step	Hyp	Ref	Expression
1		snidg	$$⊢A\in V\to A\in \left\{A\right\}$$
2		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
3		eleq2	$$⊢x=\left\{A\right\}\to \left(A\in x\leftrightarrow A\in \left\{A\right\}\right)$$
4	2 3	spcev	$$⊢A\in \left\{A\right\}\to \exists xA\in x$$
5	1 4	syl	$$⊢A\in V\to \exists xA\in x$$