Theorem sbcom3
Substituting \( y \) for \( x \) and then \( z' \) for \( y \) is equivalent to
substituting \( z' \) for both \( x \) and \( y \). Usage of this theorem is
discouraged because it depends on [ax-13]. For a version requiring a
disjoint variable, but fewer axioms, see sbcom3vv. (Contributed by
Giovanni Mascellani, 8-Apr-2018.) Remove dependency on [ax-11].
(Revised by Wolf Lammen, 16-Sep-2018.) (Proof shortened by Wolf Lammen,
16-Sep-2018.) (New usage is discouraged.)
Conclusion
\( \vdash [ z' / y ] \, [ y / x ] \, \varphi \leftrightarrow [ z' / y ] \, [ z' / x ] \, \varphi \)
Proof
l0
nfa1
drsb2
l2
sbbid l0 _
\( \vdash \forall y \, y = z' \rightarrow ([ z' / y ] \, [ y / x ] \, \varphi \leftrightarrow [ z' / y ] \, [ z' / x ] \, \varphi) \)
l3
sb4b
\( \vdash \neg \forall y \, y = z' \rightarrow ([ z' / y ] \, [ y / x ] \, \varphi \leftrightarrow \forall y \, (y = z' \rightarrow [ y / x ] \, \varphi)) \)
sbequ
pm5.74i _
albii _
\( \vdash \forall y \, (y = z' \rightarrow [ y / x ] \, \varphi) \leftrightarrow \forall y \, (y = z' \rightarrow [ z' / x ] \, \varphi) \)
l7
bitrdi l3 _
\( \vdash \neg \forall y \, y = z' \rightarrow ([ z' / y ] \, [ y / x ] \, \varphi \leftrightarrow \forall y \, (y = z' \rightarrow [ z' / x ] \, \varphi)) \)
sb4b
\( \vdash \neg \forall y \, y = z' \rightarrow ([ z' / y ] \, [ z' / x ] \, \varphi \leftrightarrow \forall y \, (y = z' \rightarrow [ z' / x ] \, \varphi)) \)
bitr4d l7 _
\( \vdash \neg \forall y \, y = z' \rightarrow ([ z' / y ] \, [ y / x ] \, \varphi \leftrightarrow [ z' / y ] \, [ z' / x ] \, \varphi) \)
pm2.61i l2 _