Theorem nfex

If \( x \) is not free in \( \varphi \), then it is not free in \( \exists y \, \varphi \). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) Reduce symbol count in nfex, hbex. (Revised by Wolf Lammen, 16-Oct-2021.)

Hypothesis
nfex.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash \Finv x \, \exists y \, \varphi \)
Proof
l0
df-ex
\( \vdash \exists y \, \varphi \leftrightarrow \neg \forall y \, \neg \varphi \)
nfex.1
nfn _
nfal _
nfn _
\( \vdash \Finv x \, (\neg \forall y \, \neg \varphi) \)
nfxfr l0 _