Theorem sn-exelALT

Description: Alternate proof of exel , avoiding ax-pr but requiring ax-5 , ax-9 , and ax-pow . This is similar to how elALT2 uses ax-pow instead of ax-pr compared to el . (Contributed by SN, 18-Sep-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sn-exelALT	|- E. y E. x x e. y

Proof

Step	Hyp	Ref	Expression
1		ax-pow	|- E. y A. x ( A. w ( w e. x -> w e. z ) -> x e. y )
2		ax6ev	|- E. x x = z
3		ax9v1	|- ( x = z -> ( w e. x -> w e. z ) )
4	3	alrimiv	|- ( x = z -> A. w ( w e. x -> w e. z ) )
5	2 4	eximii	|- E. x A. w ( w e. x -> w e. z )
6		exim	|- ( A. x ( A. w ( w e. x -> w e. z ) -> x e. y ) -> ( E. x A. w ( w e. x -> w e. z ) -> E. x x e. y ) )
7	5 6	mpi	|- ( A. x ( A. w ( w e. x -> w e. z ) -> x e. y ) -> E. x x e. y )
8	1 7	eximii	|- E. y E. x x e. y