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

Metamath Proof Explorer

Theorem sbco4lem

Description: Lemma for sbco4 . It replaces the temporary variable v with another temporary variable w . (Contributed by Jim Kingdon, 26-Sep-2018) (Proof shortened by Wolf Lammen, 12-Oct-2024) Avoid ax-11 . (Revised by SN, 3-Sep-2025)

Ref Expression
Assertion sbco4lem ⊢ x v y x v y φ ↔ x w y x w y φ

Proof

Step Hyp Ref Expression
1 sbequ ⊢ v = w → v y φ ↔ w y φ
2 1 sbbidv ⊢ v = w → y x v y φ ↔ y x w y φ
3 2 cbvsbv ⊢ x v y x v y φ ↔ x w y x w y φ