Theorem nfs1v

The setvar \( x \) is not free in \( [ y' / x ] \, \varphi \) when \( x \) and \( y' \) are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) Shorten nfs1v and hbs1 combined. (Revised by Wolf Lammen, 28-Jul-2022.)

Conclusion
\( \vdash \Finv x \, [ y' / x ] \, \varphi \)
Proof
l0
sb6
\( \vdash [ y' / x ] \, \varphi \leftrightarrow \forall x \, (x = y' \rightarrow \varphi) \)
nfa1
\( \vdash \Finv x \, \forall x \, (x = y' \rightarrow \varphi) \)
nfxfr l0 _