Theorem nfs1f

If \( x \) is not free in \( \varphi \), it is not free in \( [ y' / x ] \, \varphi \). (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis
nfs1f.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash \Finv x \, [ y' / x ] \, \varphi \)
Proof
nfs1f.1
l1
sbf _
\( \vdash [ y' / x ] \, \varphi \leftrightarrow \varphi \)
nfs1f.1
\( \vdash \Finv x \, \varphi \)
nfxfr l1 _