Theorem sb3

One direction of a simplified definition of substitution when variables are distinct. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.)

Conclusion
\( \vdash \neg \forall x \, x = y' \rightarrow \exists x \, (x = y' \wedge \varphi) \rightarrow [ y' / x ] \, \varphi \)
Proof
sb3b
biimprd _