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	⊢ ∃ 𝑦 ∃ 𝑥 𝑥 ∈ 𝑦

Proof

Step	Hyp	Ref	Expression
1		ax-pow	⊢ ∃ 𝑦 ∀ 𝑥 ( ∀ 𝑤 ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧 ) → 𝑥 ∈ 𝑦 )
2		ax6ev	⊢ ∃ 𝑥 𝑥 = 𝑧
3		ax9v1	⊢ ( 𝑥 = 𝑧 → ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧 ) )
4	3	alrimiv	⊢ ( 𝑥 = 𝑧 → ∀ 𝑤 ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧 ) )
5	2 4	eximii	⊢ ∃ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧 )
6		exim	⊢ ( ∀ 𝑥 ( ∀ 𝑤 ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧 ) → 𝑥 ∈ 𝑦 ) → ( ∃ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧 ) → ∃ 𝑥 𝑥 ∈ 𝑦 ) )
7	5 6	mpi	⊢ ( ∀ 𝑥 ( ∀ 𝑤 ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧 ) → 𝑥 ∈ 𝑦 ) → ∃ 𝑥 𝑥 ∈ 𝑦 )
8	1 7	eximii	⊢ ∃ 𝑦 ∃ 𝑥 𝑥 ∈ 𝑦