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 ⊢ y u x v u x v y φ ↔ x w y x w y φ

Proof

Step Hyp Ref Expression
1 sbequ ⊢ u = y → u x v y φ ↔ y x v y φ
2 1 sbbidv ⊢ u = y → x v u x v y φ ↔ x v y x v y φ
3 2 sbievw ⊢ y u x v u x v y φ ↔ x v y x v y φ
4 sbco4lem ⊢ x v y x v y φ ↔ x t y x t y φ
5 sbco4lem ⊢ x t y x t y φ ↔ x w y x w y φ
6 4 5 bitri ⊢ x v y x v y φ ↔ x w y x w y φ
7 3 6 bitri ⊢ y u x v u x v y φ ↔ x w y x w y φ