Theorem nfrd

Consequence of the definition of not-free in a context. (Contributed by Wolf Lammen, 15-Oct-2021.)

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