Theorem sb4e

One direction of a simplified definition of substitution that unlike sb4b does not require a distinctor antecedent. 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 \, (x = y \rightarrow \exists y \, \varphi) \)
Proof
l0
sb1
\( \vdash [ y / x ] \, \varphi \rightarrow \exists x \, (x = y \wedge \varphi) \)
equs5e
\( \vdash \exists x \, (x = y \wedge \varphi) \rightarrow \forall x \, (x = y \rightarrow \exists y \, \varphi) \)
syl l0 _