Theorem cbvsbdavw

Description: Change bound variable in proper substitution. Deduction form. (Contributed by GG, 14-Aug-2025)

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

Proof

Step	Hyp	Ref	Expression
1		cbvsbdavw.1	$$⊢\left(\phi \wedge x=y\right)\to \left(\psi \leftrightarrow \chi \right)$$
2		equequ1	$$⊢x=y\to \left(x=t\leftrightarrow y=t\right)$$
3	2	adantl	$$⊢\left(\phi \wedge x=y\right)\to \left(x=t\leftrightarrow y=t\right)$$
4	3 1	imbi12d	$$⊢\left(\phi \wedge x=y\right)\to \left(\left(x=t\to \psi \right)\leftrightarrow \left(y=t\to \chi \right)\right)$$
5	4	cbvaldvaw	$$⊢\phi \to \left(\forall x\left(x=t\to \psi \right)\leftrightarrow \forall y\left(y=t\to \chi \right)\right)$$
6	5	imbi2d	$$⊢\phi \to \left(\left(t=z\to \forall x\left(x=t\to \psi \right)\right)\leftrightarrow \left(t=z\to \forall y\left(y=t\to \chi \right)\right)\right)$$
7	6	albidv	$$⊢\phi \to \left(\forall t\left(t=z\to \forall x\left(x=t\to \psi \right)\right)\leftrightarrow \forall t\left(t=z\to \forall y\left(y=t\to \chi \right)\right)\right)$$
8		df-sb	$$⊢\left[z/x\right]\psi \leftrightarrow \forall t\left(t=z\to \forall x\left(x=t\to \psi \right)\right)$$
9		df-sb	$$⊢\left[z/y\right]\chi \leftrightarrow \forall t\left(t=z\to \forall y\left(y=t\to \chi \right)\right)$$
10	7 8 9	3bitr4g	$$⊢\phi \to \left(\left[z/x\right]\psi \leftrightarrow \left[z/y\right]\chi \right)$$