Theorem hbsb2e

Special case of a bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.)

Conclusion
\( \vdash [ y / x ] \, \varphi \rightarrow \forall x \, [ y / x ] \, \exists y \, \varphi \)
Proof
l0
sb4e
\( \vdash [ y / x ] \, \varphi \rightarrow \forall x \, (x = y \rightarrow \exists y \, \varphi) \)
sb2
axc4i _
\( \vdash \forall x \, (x = y \rightarrow \exists y \, \varphi) \rightarrow \forall x \, [ y / x ] \, \exists y \, \varphi \)
syl l0 _