Theorem nfexhe

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

Hypothesis
nfexhe.1
\( \vdash \exists x \, \varphi \rightarrow \varphi \)
Conclusion
\( \vdash \Finv x \, \exists y \, \varphi \)
Proof
l0
hbe1
l1
excomim
\( \vdash \exists x \, \exists y \, \varphi \rightarrow \exists y \, \exists x \, \varphi \)
nfexhe.1
eximi _
\( \vdash \exists y \, \exists x \, \varphi \rightarrow \exists y \, \varphi \)
syl l1 _
alrimih l0 _
nfi _