Theorem nfnf1

The setvar \( x \) is not free in \( \Finv x \, \varphi \). (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on [ax-12]. (Revised by Wolf Lammen, 12-Oct-2021.)

Conclusion
\( \vdash \Finv x \, \Finv x \, \varphi \)
Proof
l0
df-nf
\( \vdash \Finv x \, \varphi \leftrightarrow \exists x \, \varphi \rightarrow \forall x \, \varphi \)
l1
nfe1
nfa1
nfim l1 _
\( \vdash \Finv x \, (\exists x \, \varphi \rightarrow \forall x \, \varphi) \)
nfxfr l0 _