Theorem selsALT

Description: Alternate proof of sels , requiring ax-sep but not using el (which is proved from it as elALT ). (especially when the proof of el is inlined in sels ). (Contributed by NM, 4-Jan-2002) Generalize from the proof of elALT . (Revised by BJ, 3-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	selsALT	$$⊢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		snexg	$$⊢A\in \left\{A\right\}\to \left\{A\right\}\in \mathrm{V}$$
3		snidg	$$⊢A\in \left\{A\right\}\to A\in \left\{A\right\}$$
4		eleq2	$$⊢x=\left\{A\right\}\to \left(A\in x\leftrightarrow A\in \left\{A\right\}\right)$$
5	2 3 4	spcedv	$$⊢A\in \left\{A\right\}\to \exists xA\in x$$
6	1 5	syl	$$⊢A\in V\to \exists xA\in x$$