This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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