Theorem nf2

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

Conclusion
\( \vdash \Finv x \, \varphi \leftrightarrow \forall x \, \varphi \vee \neg \exists x \, \varphi \)
Proof
l0
df-nf
\( \vdash \Finv x \, \varphi \leftrightarrow \exists x \, \varphi \rightarrow \forall x \, \varphi \)
l1
imor
\( \vdash \exists x \, \varphi \rightarrow \forall x \, \varphi \leftrightarrow \neg \exists x \, \varphi \vee \forall x \, \varphi \)
orcom
\( \vdash \neg \exists x \, \varphi \vee \forall x \, \varphi \leftrightarrow \forall x \, \varphi \vee \neg \exists x \, \varphi \)
3bitri l0 l1 _