Theorem sbcom2
Commutativity law for substitution. Used in proof of Theorem 9.7 of
[Megill] p. 449 (p. 16 of the preprint). (Contributed by NM,
27-May-1997.) (Proof shortened by Wolf Lammen, 23-Dec-2022.)
Conclusion
\( \vdash [ w' / z ] \, [ y' / x ] \, \varphi \leftrightarrow [ y' / x ] \, [ w' / z ] \, \varphi \)
Proof
l0
2sb6
\( \vdash [ v / z ] \, [ u / x ] \, \varphi \leftrightarrow \forall z \, \forall x \, (z = v \wedge x = u \rightarrow \varphi) \)
l1
alcom
\( \vdash \forall z \, \forall x \, (z = v \wedge x = u \rightarrow \varphi) \leftrightarrow \forall x \, \forall z \, (z = v \wedge x = u \rightarrow \varphi) \)
ancomst
2albii _
\( \vdash \forall x \, \forall z \, (z = v \wedge x = u \rightarrow \varphi) \leftrightarrow \forall x \, \forall z \, (x = u \wedge z = v \rightarrow \varphi) \)
l4
3bitri l0 l1 _
\( \vdash [ v / z ] \, [ u / x ] \, \varphi \leftrightarrow \forall x \, \forall z \, (x = u \wedge z = v \rightarrow \varphi) \)
2sb6
\( \vdash [ u / x ] \, [ v / z ] \, \varphi \leftrightarrow \forall x \, \forall z \, (x = u \wedge z = v \rightarrow \varphi) \)
l6
bitr4i l4 _
\( \vdash [ v / z ] \, [ u / x ] \, \varphi \leftrightarrow [ u / x ] \, [ v / z ] \, \varphi \)
sbequ
sbbidv _
\( \vdash u = y' \rightarrow ([ v / z ] \, [ u / x ] \, \varphi \leftrightarrow [ v / z ] \, [ y' / x ] \, \varphi) \)
l9
bitr3id l6 _
\( \vdash u = y' \rightarrow ([ u / x ] \, [ v / z ] \, \varphi \leftrightarrow [ v / z ] \, [ y' / x ] \, \varphi) \)
sbequ
\( \vdash v = w' \rightarrow ([ v / z ] \, [ y' / x ] \, \varphi \leftrightarrow [ w' / z ] \, [ y' / x ] \, \varphi) \)
l11
sylan9bb l9 _
\( \vdash u = y' \wedge v = w' \rightarrow ([ u / x ] \, [ v / z ] \, \varphi \leftrightarrow [ w' / z ] \, [ y' / x ] \, \varphi) \)
sbequ
l13
sbbidv _
\( \vdash v = w' \rightarrow ([ u / x ] \, [ v / z ] \, \varphi \leftrightarrow [ u / x ] \, [ w' / z ] \, \varphi) \)
sbequ
\( \vdash u = y' \rightarrow ([ u / x ] \, [ w' / z ] \, \varphi \leftrightarrow [ y' / x ] \, [ w' / z ] \, \varphi) \)
sylan9bbr l13 _
\( \vdash u = y' \wedge v = w' \rightarrow ([ u / x ] \, [ v / z ] \, \varphi \leftrightarrow [ y' / x ] \, [ w' / z ] \, \varphi) \)
bitr3d l11 _
l17
ex _
\( \vdash u = y' \rightarrow v = w' \rightarrow ([ w' / z ] \, [ y' / x ] \, \varphi \leftrightarrow [ y' / x ] \, [ w' / z ] \, \varphi) \)
ax6ev
\( \vdash \exists u \, u = y' \)
l19
exlimiiv l17 _
\( \vdash v = w' \rightarrow ([ w' / z ] \, [ y' / x ] \, \varphi \leftrightarrow [ y' / x ] \, [ w' / z ] \, \varphi) \)
ax6ev
\( \vdash \exists v \, v = w' \)
exlimiiv l19 _