Theorem nfs1

If \( y \) is not free in \( \varphi \), \( x \) is not free in \( [ y / x ] \, \varphi \). Usage of this theorem is discouraged because it depends on [ax-13]. Check out nfs1v for a version requiring fewer axioms. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)

Hypothesis
nfs1.1
\( \vdash \Finv y \, \varphi \)
Conclusion
\( \vdash \Finv x \, [ y / x ] \, \varphi \)
Proof
nfs1.1
nf5ri _
hbsb3 _
nf5i _