Theorem nfri

Consequence of the definition of not-free. (Contributed by Wolf Lammen, 16-Sep-2021.)

Hypothesis
nfri.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash \exists x \, \varphi \rightarrow \forall x \, \varphi \)
Proof
l0
nfri.1
\( \vdash \Finv x \, \varphi \)
df-nf
\( \vdash \Finv x \, \varphi \leftrightarrow \exists x \, \varphi \rightarrow \forall x \, \varphi \)
mpbi l0 _