Theorem nfexhe

Description: Version of nfex with the existential dual to the 'h' hypothesis, avoiding ax-12 . (Contributed by SN, 11-Feb-2026)

	Ref	Expression
Hypothesis	nfexhe.1	⊢ ( ∃ 𝑥 𝜑 → 𝜑 )
Assertion	nfexhe	⊢ Ⅎ 𝑥 ∃ 𝑦 𝜑

Proof

Step	Hyp	Ref	Expression
1		nfexhe.1	⊢ ( ∃ 𝑥 𝜑 → 𝜑 )
2		hbe1	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑥 ∃ 𝑦 𝜑 )
3		excomim	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 → ∃ 𝑦 ∃ 𝑥 𝜑 )
4	1	eximi	⊢ ( ∃ 𝑦 ∃ 𝑥 𝜑 → ∃ 𝑦 𝜑 )
5	3 4	syl	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 → ∃ 𝑦 𝜑 )
6	2 5	alrimih	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 )
7	6	nfi	⊢ Ⅎ 𝑥 ∃ 𝑦 𝜑