Theorem nfnbi

A variable is nonfree in a proposition if and only if it is so in its negation. (Contributed by BJ, 6-May-2019.) (Proof shortened by Wolf Lammen, 6-Oct-2024.)

Conclusion
\( \vdash \Finv x \, \varphi \leftrightarrow \Finv x \, (\neg \varphi) \)
Proof
exnal
l1
imbi1i _
\( \vdash \exists x \, \neg \varphi \rightarrow \forall x \, \neg \varphi \leftrightarrow \neg \forall x \, \varphi \rightarrow \forall x \, \neg \varphi \)
l2
df-nf
\( \vdash \Finv x \, (\neg \varphi) \leftrightarrow \exists x \, \neg \varphi \rightarrow \forall x \, \neg \varphi \)
nf4
\( \vdash \Finv x \, \varphi \leftrightarrow \neg \forall x \, \varphi \rightarrow \forall x \, \neg \varphi \)
3bitr4ri l1 l2 _