Theorem hbsb3

If \( y \) is not free in \( \varphi \), \( x \) is not free in \( [ y / x ] \, \varphi \). Usage of this theorem is discouraged because it depends on [ax-13]. Check out [bj-hbsb3v] for a weaker version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (New usage is discouraged.)

Hypothesis
hbsb3.1
\( \vdash \varphi \rightarrow \forall y \, \varphi \)
Conclusion
\( \vdash [ y / x ] \, \varphi \rightarrow \forall x \, [ y / x ] \, \varphi \)
Proof
hbsb3.1
l1
sbimi _
\( \vdash [ y / x ] \, \varphi \rightarrow [ y / x ] \, \forall y \, \varphi \)
hbsb2a
\( \vdash [ y / x ] \, \forall y \, \varphi \rightarrow \forall x \, [ y / x ] \, \varphi \)
syl l1 _