Theorem nf4

Alternate definition of nonfreeness. This definition uses only primitive symbols ( -> , -. , A. ). (Contributed by BJ, 16-Sep-2021.)

Conclusion
\( \vdash \Finv x \, \varphi \leftrightarrow \neg \forall x \, \varphi \rightarrow \forall x \, \neg \varphi \)
Proof
l0
nf3
\( \vdash \Finv x \, \varphi \leftrightarrow \forall x \, \varphi \vee \forall x \, \neg \varphi \)
df-or
\( \vdash \forall x \, \varphi \vee \forall x \, \neg \varphi \leftrightarrow \neg \forall x \, \varphi \rightarrow \forall x \, \neg \varphi \)
bitri l0 _