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 ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbequ | |- ( v = w -> ( [ v / y ] ph <-> [ w / y ] ph ) ) |
|
| 2 | 1 | sbbidv | |- ( v = w -> ( [ y / x ] [ v / y ] ph <-> [ y / x ] [ w / y ] ph ) ) |
| 3 | 2 | cbvsbv | |- ( [ x / v ] [ y / x ] [ v / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph ) |