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

Proof

Step	Hyp	Ref	Expression
1		ax-pow	$$⊢\exists y\forall x\left(\forall w\left(w\in x\to w\in z\right)\to x\in y\right)$$
2		ax6ev	$$⊢\exists xx=z$$
3		ax9v1	$$⊢x=z\to \left(w\in x\to w\in z\right)$$
4	3	alrimiv	$$⊢x=z\to \forall w\left(w\in x\to w\in z\right)$$
5	2 4	eximii	$$⊢\exists x\forall w\left(w\in x\to w\in z\right)$$
6		exim	$$⊢\forall x\left(\forall w\left(w\in x\to w\in z\right)\to x\in y\right)\to \left(\exists x\forall w\left(w\in x\to w\in z\right)\to \exists xx\in y\right)$$
7	5 6	mpi	$$⊢\forall x\left(\forall w\left(w\in x\to w\in z\right)\to x\in y\right)\to \exists xx\in y$$
8	1 7	eximii	$$⊢\exists y\exists xx\in y$$