Theorem sb6a

Equivalence for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Sep-2018.)

Conclusion
\( \vdash [ y / x ] \, \varphi \leftrightarrow \forall x \, (x = y \rightarrow [ x / y ] \, \varphi) \)
Proof
l0
sbcov
\( \vdash [ y / x ] \, [ x / y ] \, \varphi \leftrightarrow [ y / x ] \, \varphi \)
sb6
\( \vdash [ y / x ] \, [ x / y ] \, \varphi \leftrightarrow \forall x \, (x = y \rightarrow [ x / y ] \, \varphi) \)
bitr3i l0 _