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	|- ( E. x ph -> ph )
Assertion	nfexhe	|- F/ x E. y ph

Proof

Step	Hyp	Ref	Expression
1		nfexhe.1	|- ( E. x ph -> ph )
2		hbe1	|- ( E. x E. y ph -> A. x E. x E. y ph )
3		excomim	|- ( E. x E. y ph -> E. y E. x ph )
4	1	eximi	|- ( E. y E. x ph -> E. y ph )
5	3 4	syl	|- ( E. x E. y ph -> E. y ph )
6	2 5	alrimih	|- ( E. x E. y ph -> A. x E. y ph )
7	6	nfi	|- F/ x E. y ph