Theorem nfexd2

Variation on nfexd which adds the hypothesis that \( x \) and \( y \) are distinct in the inner subproof. (Contributed by Mario Carneiro, 8-Oct-2016.) Usage of this theorem is discouraged because it depends on [ax-13]. Use nfexd instead. (New usage is discouraged.)

Hypotheses
nfald2.1
\( \vdash \Finv y \, \varphi \)
nfald2.2
\( \vdash \varphi \wedge \neg \forall x \, x = y \rightarrow \Finv x \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \Finv x \, \exists y \, \psi \)
Proof
l0
df-ex
\( \vdash \exists y \, \psi \leftrightarrow \neg \forall y \, \neg \psi \)
l1
nfald2.1
nfald2.2
nfnd _
nfald2 l1 _
nfnd _
\( \vdash \varphi \rightarrow \Finv x \, (\neg \forall y \, \neg \psi) \)
nfxfrd l0 _