Theorem nf6

An alternate definition of [df-nf]. (Contributed by Mario Carneiro, 24-Sep-2016.)

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