Theorem cbvsbv

Description: Change the bound variable (i.e. the substituted one) in wff's linked by implicit substitution. The proof was extracted from a former cbvabv version. (Contributed by Wolf Lammen, 16-Mar-2025)

	Ref	Expression
Hypothesis	cbvsbv.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	cbvsbv	$$⊢\left[z/x\right]\phi \leftrightarrow \left[z/y\right]\psi$$

Proof

Step	Hyp	Ref	Expression
1		cbvsbv.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		sbco2vv	$$⊢\left[z/y\right]\left[y/x\right]\phi \leftrightarrow \left[z/x\right]\phi$$
3	1	sbievw	$$⊢\left[y/x\right]\phi \leftrightarrow \psi$$
4	3	sbbii	$$⊢\left[z/y\right]\left[y/x\right]\phi \leftrightarrow \left[z/y\right]\psi$$
5	2 4	bitr3i	$$⊢\left[z/x\right]\phi \leftrightarrow \left[z/y\right]\psi$$