This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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