Theorem sb1v

One direction of sb5, provable from fewer axioms. Version of sb1 with a disjoint variable condition using fewer axioms. (Contributed by NM, 13-May-1993.) (Revised by Wolf Lammen, 20-Jan-2024.)

Conclusion
\( \vdash [ y' / x ] \, \varphi \rightarrow \exists x \, (x = y' \wedge \varphi) \)
Proof
l0
sb6
\( \vdash [ y' / x ] \, \varphi \leftrightarrow \forall x \, (x = y' \rightarrow \varphi) \)
equs4v
\( \vdash \forall x \, (x = y' \rightarrow \varphi) \rightarrow \exists x \, (x = y' \wedge \varphi) \)
sylbi l0 _