Theorem sbelx

Elimination of substitution. Also see sbel2x. (Contributed by NM, 5-Aug-1993.) Avoid [ax-13]. (Revised by Wolf Lammen, 6-Aug-2023.) Avoid [ax-10]. (Revised by GG, 20-Aug-2023.)

Conclusion
\( \vdash \varphi \leftrightarrow \exists x \, (x = y \wedge [ x / y ] \, \varphi) \)
Proof
sbequ12r
equsexvw _
bicomi _