Theorem nfexd

If \( x \) is not free in \( \psi \), then it is not free in \( \exists y \, \psi \). (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypotheses
nfald.1
\( \vdash \Finv y \, \varphi \)
nfald.2
\( \vdash \varphi \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
nfald.1
nfald.2
nfnd _
nfald l1 _
nfnd _
\( \vdash \varphi \rightarrow \Finv x \, (\neg \forall y \, \neg \psi) \)
nfxfrd l0 _