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	|- E. y x e. y

Proof

Step	Hyp	Ref	Expression
1		zfpow	|- E. y A. z ( A. y ( y e. z -> y e. x ) -> z e. y )
2		ax9	|- ( z = x -> ( y e. z -> y e. x ) )
3	2	alrimiv	|- ( z = x -> A. y ( y e. z -> y e. x ) )
4		ax8	|- ( z = x -> ( z e. y -> x e. y ) )
5	3 4	embantd	|- ( z = x -> ( ( A. y ( y e. z -> y e. x ) -> z e. y ) -> x e. y ) )
6	5	spimvw	|- ( A. z ( A. y ( y e. z -> y e. x ) -> z e. y ) -> x e. y )
7	1 6	eximii	|- E. y x e. y