Theorem sn-el

Description: A version of el with an inner existential quantifier on x , which avoids ax-7 and ax-8 . (Contributed by SN, 18-Sep-2023)

	Ref	Expression
Assertion	sn-el	|- 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