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	⊢ ( [ 𝑦 / 𝑢 ] [ 𝑥 / 𝑣 ] [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑤 ] [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbequ	⊢ ( 𝑢 = 𝑦 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
2	1	sbbidv	⊢ ( 𝑢 = 𝑦 → ( [ 𝑥 / 𝑣 ] [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑣 ] [ 𝑦 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
3	2	sbievw	⊢ ( [ 𝑦 / 𝑢 ] [ 𝑥 / 𝑣 ] [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑣 ] [ 𝑦 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )
4		sbco4lem	⊢ ( [ 𝑥 / 𝑣 ] [ 𝑦 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑡 ] [ 𝑦 / 𝑥 ] [ 𝑡 / 𝑦 ] 𝜑 )
5		sbco4lem	⊢ ( [ 𝑥 / 𝑡 ] [ 𝑦 / 𝑥 ] [ 𝑡 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑤 ] [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
6	4 5	bitri	⊢ ( [ 𝑥 / 𝑣 ] [ 𝑦 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑤 ] [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
7	3 6	bitri	⊢ ( [ 𝑦 / 𝑢 ] [ 𝑥 / 𝑣 ] [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑤 ] [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )