Theorem nf5i

Deduce that \( x \) is not free in \( \varphi \) from the definition. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis
nf5i.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
Conclusion
\( \vdash \Finv x \, \varphi \)
Proof
l0
nf5-1
\( \vdash \forall x \, (\varphi \rightarrow \forall x \, \varphi) \rightarrow \Finv x \, \varphi \)
nf5i.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
mpg l0 _