Theorem nfsbv

If \( z \) is not free in \( \varphi \), then it is not free in \( [ y' / x ] \, \varphi \) when \( z \) is disjoint from both \( x \) and \( y' \). Version of nfsb with an additional disjoint variable condition on x , z but not requiring [ax-13]. (Contributed by Mario Carneiro, 11-Aug-2016.) (Revised by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on x , y. (Revised by Steven Nguyen, 13-Aug-2023.) (Proof shortened by Wolf Lammen, 25-Oct-2024.)

Hypothesis
nfsbv.nf
\( \vdash \Finv z \, \varphi \)
Conclusion
\( \vdash \Finv z \, [ y' / x ] \, \varphi \)
Proof
nfsbv.nf
nf5ri _
hbsbw _
nf5i _