# Metamath Proof Explorer

## 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}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {y}$

### Proof

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