Theorem nf5

Alternate definition of [df-nf]. (Contributed by Mario Carneiro, 11-Aug-2016.) [df-nf] changed. (Revised by Wolf Lammen, 11-Sep-2021.)

Conclusion
\( \vdash \Finv x \, \varphi \leftrightarrow \forall x \, (\varphi \rightarrow \forall x \, \varphi) \)
Proof
l0
df-nf
\( \vdash \Finv x \, \varphi \leftrightarrow \exists x \, \varphi \rightarrow \forall x \, \varphi \)
nfa1
19.23 _
\( \vdash \forall x \, (\varphi \rightarrow \forall x \, \varphi) \leftrightarrow \exists x \, \varphi \rightarrow \forall x \, \varphi \)
bitr4i l0 _