Theorem nf3

Alternate definition of nonfreeness. (Contributed by BJ, 16-Sep-2021.)

Conclusion
\( \vdash \Finv x \, \varphi \leftrightarrow \forall x \, \varphi \vee \forall x \, \neg \varphi \)
Proof
l0
nf2
\( \vdash \Finv x \, \varphi \leftrightarrow \forall x \, \varphi \vee \neg \exists x \, \varphi \)
alnex
orbi2i _
\( \vdash \forall x \, \varphi \vee \forall x \, \neg \varphi \leftrightarrow \forall x \, \varphi \vee \neg \exists x \, \varphi \)
bitr4i l0 _