Theorem nfi

Deduce that \( x \) is not free in \( \varphi \) from the definition. (Contributed by Wolf Lammen, 15-Sep-2021.)

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