Theorem nfnt

If a variable is nonfree in a proposition, then it is nonfree in its negation. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 28-Dec-2017.) (Revised by BJ, 24-Jul-2019.) [df-nf] changed. (Revised by Wolf Lammen, 4-Oct-2021.)

Conclusion
\( \vdash \Finv x \, \varphi \rightarrow \Finv x \, (\neg \varphi) \)
Proof
nfnbi
biimpi _