Theorem sbco4

Description: 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)

	Ref	Expression
Assertion	sbco4	|- ( [ y / u ] [ x / v ] [ u / x ] [ v / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph )

Proof

Step	Hyp	Ref	Expression
1		sbequ	|- ( u = y -> ( [ u / x ] [ v / y ] ph <-> [ y / x ] [ v / y ] ph ) )
2	1	sbbidv	|- ( u = y -> ( [ x / v ] [ u / x ] [ v / y ] ph <-> [ x / v ] [ y / x ] [ v / y ] ph ) )
3	2	sbievw	|- ( [ y / u ] [ x / v ] [ u / x ] [ v / y ] ph <-> [ x / v ] [ y / x ] [ v / y ] ph )
4		sbco4lem	|- ( [ x / v ] [ y / x ] [ v / y ] ph <-> [ x / t ] [ y / x ] [ t / y ] ph )
5		sbco4lem	|- ( [ x / t ] [ y / x ] [ t / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph )
6	4 5	bitri	|- ( [ x / v ] [ y / x ] [ v / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph )
7	3 6	bitri	|- ( [ y / u ] [ x / v ] [ u / x ] [ v / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph )