This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 e. V -> E. x A e. x )

Proof

Step	Hyp	Ref	Expression
1		eleq1	\|- ( y = A -> ( y e. x <-> A e. x ) )
2	1	exbidv	\|- ( y = A -> ( E. x y e. x <-> E. x A e. x ) )
3		el	\|- E. x y e. x
4	2 3	vtoclg	\|- ( A e. V -> E. x A e. x )