Theorem nfal

If \( x \) is not free in \( \varphi \), then it is not free in \( \forall y \, \varphi \). (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis
nfal.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash \Finv x \, \forall y \, \varphi \)
Proof
nfal.1
nf5ri _
hbal _
nf5i _