Theorem hbsbw

If \( z \) is not free in \( \varphi \), it is not free in \( [ y' / x ] \, \varphi \) when \( y' \) and \( z \) are distinct. Version of hbsb with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 12-Aug-1993.) Remove dependencies on axioms. (Revised by GG, 23-May-2024.) (Proof shortened by Wolf Lammen, 14-May-2025.)

Hypothesis
hbsbw.1
\( \vdash \varphi \rightarrow \forall z \, \varphi \)
Conclusion
\( \vdash [ y' / x ] \, \varphi \rightarrow \forall z \, [ y' / x ] \, \varphi \)
Proof
hbsbw.1
l1
sbimi _
\( \vdash [ y' / x ] \, \varphi \rightarrow [ y' / x ] \, \forall z \, \varphi \)
sbal
\( \vdash [ y' / x ] \, \forall z \, \varphi \leftrightarrow \forall z \, [ y' / x ] \, \varphi \)
sylib l1 _