Theorem nf5ri

Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 15-Mar-2023.)

Hypothesis
nf5ri.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
Proof
nf5ri.1
nfri _
\( \vdash \exists x \, \varphi \rightarrow \forall x \, \varphi \)
19.23bi _