Theorem sbequbidv

Description: Deduction substituting both sides of a biconditional. (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	sbequbidv.1	$$⊢\phi \to u=v$$
	sbequbidv.2	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
Assertion	sbequbidv	$$⊢\phi \to \left(\left[u/x\right]\psi \leftrightarrow \left[v/x\right]\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbequbidv.1	$$⊢\phi \to u=v$$
2		sbequbidv.2	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
3		equequ2	$$⊢u=v\to \left(t=u\leftrightarrow t=v\right)$$
4	1 3	syl	$$⊢\phi \to \left(t=u\leftrightarrow t=v\right)$$
5	2	imbi2d	$$⊢\phi \to \left(\left(x=t\to \psi \right)\leftrightarrow \left(x=t\to \chi \right)\right)$$
6	5	albidv	$$⊢\phi \to \left(\forall x\left(x=t\to \psi \right)\leftrightarrow \forall x\left(x=t\to \chi \right)\right)$$
7	4 6	imbi12d	$$⊢\phi \to \left(\left(t=u\to \forall x\left(x=t\to \psi \right)\right)\leftrightarrow \left(t=v\to \forall x\left(x=t\to \chi \right)\right)\right)$$
8	7	albidv	$$⊢\phi \to \left(\forall t\left(t=u\to \forall x\left(x=t\to \psi \right)\right)\leftrightarrow \forall t\left(t=v\to \forall x\left(x=t\to \chi \right)\right)\right)$$
9		df-sb	$$⊢\left[u/x\right]\psi \leftrightarrow \forall t\left(t=u\to \forall x\left(x=t\to \psi \right)\right)$$
10		df-sb	$$⊢\left[v/x\right]\chi \leftrightarrow \forall t\left(t=v\to \forall x\left(x=t\to \chi \right)\right)$$
11	8 9 10	3bitr4g	$$⊢\phi \to \left(\left[u/x\right]\psi \leftrightarrow \left[v/x\right]\chi \right)$$