Theorem hbsb2

Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 14-May-1993.) (New usage is discouraged.)

Conclusion
\( \vdash \neg \forall x \, x = y' \rightarrow [ y' / x ] \, \varphi \rightarrow \forall x \, [ y' / x ] \, \varphi \)
Proof
l0
sb4b
\( \vdash \neg \forall x \, x = y' \rightarrow ([ y' / x ] \, \varphi \leftrightarrow \forall x \, (x = y' \rightarrow \varphi)) \)
sb2
axc4i _
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \rightarrow \forall x \, [ y' / x ] \, \varphi \)
biimtrdi l0 _