Theorem nf5r

Consequence of the definition of not-free. (Contributed by Mario Carneiro, 26-Sep-2016.) [df-nf] changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by Wolf Lammen, 23-Nov-2023.)

Conclusion
\( \vdash \Finv x \, \varphi \rightarrow \varphi \rightarrow \forall x \, \varphi \)
Proof
l0
19.8a
\( \vdash \varphi \rightarrow \exists x \, \varphi \)
id
nfrd _
\( \vdash \Finv x \, \varphi \rightarrow \exists x \, \varphi \rightarrow \forall x \, \varphi \)
syl5 l0 _