Theorem elALT

Description: Alternate proof of el , shorter but requiring more axioms. (Contributed by NM, 4-Jan-2002) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	elALT	|- E. y x e. y

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2	1	snid	|- x e. { x }
3		snex	|- { x } e. _V
4		eleq2	|- ( y = { x } -> ( x e. y <-> x e. { x } ) )
5	3 4	spcev	|- ( x e. { x } -> E. y x e. y )
6	2 5	ax-mp	|- E. y x e. y