Theorem dfsb7

An alternate definition of proper substitution [df-sb]. By introducing a dummy variable \( y \) in the definiens, we are able to eliminate any distinct variable restrictions among the variables \( t' \), \( x \), and \( \varphi \) of the definiendum. No distinct variable conflicts arise because \( y \) effectively insulates \( t' \) from \( x \). To achieve this, we use a chain of two substitutions in the form of sb5, first \( y \) for \( x \) then \( t' \) for \( y \). Compare Definition 2.1'' of [Quine] p. 17, which is obtained from this theorem by applying [df-clab]. Theorem sb7h provides a version where \( \varphi \) and \( y \) don't have to be distinct. (Contributed by NM, 28-Jan-2004.) Revise [df-sb]. (Revised by BJ, 25-Dec-2020.) (Proof shortened by Wolf Lammen, 3-Sep-2023.)

Conclusion
\( \vdash [ t' / x ] \, \varphi \leftrightarrow \exists y \, (y = t' \wedge \exists x \, (x = y \wedge \varphi)) \)
Proof
l0
sbalex
\( \vdash \exists y \, (y = t' \wedge \forall x \, (x = y \rightarrow \varphi)) \leftrightarrow \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \)
sbalex
anbi2i _
l3
exbii _
\( \vdash \exists y \, (y = t' \wedge \exists x \, (x = y \wedge \varphi)) \leftrightarrow \exists y \, (y = t' \wedge \forall x \, (x = y \rightarrow \varphi)) \)
dfsb
\( \vdash [ t' / x ] \, \varphi \leftrightarrow \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \)
3bitr4ri l0 l3 _