Theorem nfa1

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

Conclusion
\( \vdash \Finv x \, \forall x \, \varphi \)
Proof
l0
alex
\( \vdash \forall x \, \varphi \leftrightarrow \neg \exists x \, \neg \varphi \)
nfe1
nfn _
\( \vdash \Finv x \, (\neg \exists x \, \neg \varphi) \)
nfxfr l0 _