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	$$⊢\left[x/v\right]\left[y/x\right]\left[v/y\right]\phi \leftrightarrow \left[x/w\right]\left[y/x\right]\left[w/y\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		sbequ	$$⊢v=w\to \left(\left[v/y\right]\phi \leftrightarrow \left[w/y\right]\phi \right)$$
2	1	sbbidv	$$⊢v=w\to \left(\left[y/x\right]\left[v/y\right]\phi \leftrightarrow \left[y/x\right]\left[w/y\right]\phi \right)$$
3	2	cbvsbv	$$⊢\left[x/v\right]\left[y/x\right]\left[v/y\right]\phi \leftrightarrow \left[x/w\right]\left[y/x\right]\left[w/y\right]\phi$$