Theorem nfsb

If \( z \) is not free in \( \varphi \), then it is not free in \( [ y' / x ] \, \varphi \) when \( y' \) and \( z \) are distinct. See nfsbv for a version with an additional disjoint variable condition on x , z but not requiring [ax-13]. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Feb-2024.) Usage of this theorem is discouraged because it depends on [ax-13]. Use nfsbv instead. (New usage is discouraged.)

Hypothesis
nfsb.1
\( \vdash \Finv z \, \varphi \)
Conclusion
\( \vdash \Finv z \, [ y' / x ] \, \varphi \)
Proof
l0
nftru
nfsb.1
a1i _
nfsbd l0 _
mptru _