Theorem hbsb

If \( z \) is not free in \( \varphi \), then it is not free in \( [ y' / x ] \, \varphi \) when \( y' \) and \( z \) are distinct. (Contributed by NM, 12-Aug-1993.) Usage of this theorem is discouraged because it depends on [ax-13]. Use hbsbw instead. (New usage is discouraged.)

Hypothesis
hbsb.1
\( \vdash \varphi \rightarrow \forall z \, \varphi \)
Conclusion
\( \vdash [ y' / x ] \, \varphi \rightarrow \forall z \, [ y' / x ] \, \varphi \)
Proof
hbsb.1
nf5i _
nfsb _
nf5ri _