Theorem sbco4
Two ways of exchanging two variables. Both sides of the biconditional
exchange \( x \) and \( y \), either via two temporary variables \( u \) and
\( v \), or a single temporary \( w \). (Contributed by Jim Kingdon,
25-Sep-2018.) Avoid [ax-11]. (Revised by SN, 3-Sep-2025.)
Conclusion
\( \vdash [ y / u ] \, [ x / v ] \, [ u / x ] \, [ v / y ] \, \varphi \leftrightarrow [ x / w ] \, [ y / x ] \, [ w / y ] \, \varphi \)
Proof
sbequ
sbbidv _
l2
sbievw _
\( \vdash [ y / u ] \, [ x / v ] \, [ u / x ] \, [ v / y ] \, \varphi \leftrightarrow [ x / v ] \, [ y / x ] \, [ v / y ] \, \varphi \)
l3
sbco4lem
\( \vdash [ x / v ] \, [ y / x ] \, [ v / y ] \, \varphi \leftrightarrow [ x / t ] \, [ y / x ] \, [ t / y ] \, \varphi \)
sbco4lem
\( \vdash [ x / t ] \, [ y / x ] \, [ t / y ] \, \varphi \leftrightarrow [ x / w ] \, [ y / x ] \, [ w / y ] \, \varphi \)
3bitri l2 l3 _