Theorem elALT2

Description: Alternate proof of el using ax-9 and ax-pow instead of ax-pr . (Contributed by NM, 4-Jan-2002) (Proof shortened by Andrew Salmon, 25-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	elALT2	$$⊢\exists yx\in y$$

Proof

Step	Hyp	Ref	Expression
1		zfpow	$$⊢\exists y\forall z\left(\forall y\left(y\in z\to y\in x\right)\to z\in y\right)$$
2		ax9	$$⊢z=x\to \left(y\in z\to y\in x\right)$$
3	2	alrimiv	$$⊢z=x\to \forall y\left(y\in z\to y\in x\right)$$
4		ax8	$$⊢z=x\to \left(z\in y\to x\in y\right)$$
5	3 4	embantd	$$⊢z=x\to \left(\left(\forall y\left(y\in z\to y\in x\right)\to z\in y\right)\to x\in y\right)$$
6	5	spimvw	$$⊢\forall z\left(\forall y\left(y\in z\to y\in x\right)\to z\in y\right)\to x\in y$$
7	1 6	eximii	$$⊢\exists yx\in y$$