Theorem sb6

Alternate definition of substitution when variables are disjoint. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70. The implication "to the left" also holds without a disjoint variable condition ( sb2 ). Theorem sb6f replaces the disjoint variable condition with a nonfreeness hypothesis. Theorem sb4b replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise [df-sb]. (Revised by BJ, 22-Dec-2020.) Remove use of [ax-11]. (Revised by Steven Nguyen, 7-Jul-2023.) (Proof shortened by Wolf Lammen, 16-Jul-2023.)

Conclusion
\( \vdash [ t' / x ] \, \varphi \leftrightarrow \forall x \, (x = t' \rightarrow \varphi) \)
Proof
l0
dfsb
\( \vdash [ t' / x ] \, \varphi \leftrightarrow \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \)
equequ2
imbi1d _
albidv _
equsalvw _
\( \vdash \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \leftrightarrow \forall x \, (x = t' \rightarrow \varphi) \)
bitri l0 _