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	$$⊢\exists yx\in y$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	snid	$$⊢x\in \left\{x\right\}$$
3		snex	$$⊢\left\{x\right\}\in \mathrm{V}$$
4		eleq2	$$⊢y=\left\{x\right\}\to \left(x\in y\leftrightarrow x\in \left\{x\right\}\right)$$
5	3 4	spcev	$$⊢x\in \left\{x\right\}\to \exists yx\in y$$
6	2 5	ax-mp	$$⊢\exists yx\in y$$