Theorem nfnf

If \( x \) is not free in \( \varphi \), then it is not free in \( \Finv y \, \varphi \). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)

Hypothesis
nfnf.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash \Finv x \, \Finv y \, \varphi \)
Proof
l0
df-nf
\( \vdash \Finv y \, \varphi \leftrightarrow \exists y \, \varphi \rightarrow \forall y \, \varphi \)
nfnf.1
l2
nfex _
nfnf.1
nfal _
nfim l2 _
\( \vdash \Finv x \, (\exists y \, \varphi \rightarrow \forall y \, \varphi) \)
nfxfr l0 _