Theorem sels

Description: If a class is a set, then it is a member of a set. (Contributed by NM, 4-Jan-2002) Generalize from the proof of elALT . (Revised by BJ, 3-Apr-2019) Avoid ax-sep , ax-nul , ax-pow . (Revised by BTernaryTau, 15-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢y=A\to \left(y\in x\leftrightarrow A\in x\right)$$
2	1	exbidv	$$⊢y=A\to \left(\exists xy\in x\leftrightarrow \exists xA\in x\right)$$
3		el	$$⊢\exists xy\in x$$
4	2 3	vtoclg	$$⊢A\in V\to \exists xA\in x$$