Theorem sb5

Alternate definition of substitution when variables are disjoint. Similar to Theorem 6.1 of [Quine] p. 40. The implication "to the right" is sb1v and even needs no disjoint variable condition, see sb1. Theorem sb5f replaces the disjoint variable condition with a nonfreeness hypothesis. (Contributed by NM, 18-Aug-1993.) (Revised by Wolf Lammen, 4-Sep-2023.)

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