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	$$⊢\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$$