Theorem sbequbidv

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

	Ref	Expression
Hypotheses	sbequbidv.1	|- ( ph -> u = v )
	sbequbidv.2	|- ( ph -> ( ps <-> ch ) )
Assertion	sbequbidv	|- ( ph -> ( [ u / x ] ps <-> [ v / x ] ch ) )

Proof

Step	Hyp	Ref	Expression
1		sbequbidv.1	|- ( ph -> u = v )
2		sbequbidv.2	|- ( ph -> ( ps <-> ch ) )
3		equequ2	|- ( u = v -> ( t = u <-> t = v ) )
4	1 3	syl	|- ( ph -> ( t = u <-> t = v ) )
5	2	imbi2d	|- ( ph -> ( ( x = t -> ps ) <-> ( x = t -> ch ) ) )
6	5	albidv	|- ( ph -> ( A. x ( x = t -> ps ) <-> A. x ( x = t -> ch ) ) )
7	4 6	imbi12d	|- ( ph -> ( ( t = u -> A. x ( x = t -> ps ) ) <-> ( t = v -> A. x ( x = t -> ch ) ) ) )
8	7	albidv	|- ( ph -> ( A. t ( t = u -> A. x ( x = t -> ps ) ) <-> A. t ( t = v -> A. x ( x = t -> ch ) ) ) )
9		df-sb	|- ( [ u / x ] ps <-> A. t ( t = u -> A. x ( x = t -> ps ) ) )
10		df-sb	|- ( [ v / x ] ch <-> A. t ( t = v -> A. x ( x = t -> ch ) ) )
11	8 9 10	3bitr4g	|- ( ph -> ( [ u / x ] ps <-> [ v / x ] ch ) )