Theorem cbvsbdavw2

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

	Ref	Expression
Hypotheses	cbvsbdavw2.1	|- ( ph -> z = w )
	cbvsbdavw2.2	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
Assertion	cbvsbdavw2	|- ( ph -> ( [ z / x ] ps <-> [ w / y ] ch ) )

Proof

Step	Hyp	Ref	Expression
1		cbvsbdavw2.1	|- ( ph -> z = w )
2		cbvsbdavw2.2	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
3		equequ2	|- ( z = w -> ( t = z <-> t = w ) )
4	1 3	syl	|- ( ph -> ( t = z <-> t = w ) )
5		equequ1	|- ( x = y -> ( x = t <-> y = t ) )
6	5	adantl	|- ( ( ph /\ x = y ) -> ( x = t <-> y = t ) )
7	6 2	imbi12d	|- ( ( ph /\ x = y ) -> ( ( x = t -> ps ) <-> ( y = t -> ch ) ) )
8	7	cbvaldvaw	|- ( ph -> ( A. x ( x = t -> ps ) <-> A. y ( y = t -> ch ) ) )
9	4 8	imbi12d	|- ( ph -> ( ( t = z -> A. x ( x = t -> ps ) ) <-> ( t = w -> A. y ( y = t -> ch ) ) ) )
10	9	albidv	|- ( ph -> ( A. t ( t = z -> A. x ( x = t -> ps ) ) <-> A. t ( t = w -> A. y ( y = t -> ch ) ) ) )
11		df-sb	|- ( [ z / x ] ps <-> A. t ( t = z -> A. x ( x = t -> ps ) ) )
12		df-sb	|- ( [ w / y ] ch <-> A. t ( t = w -> A. y ( y = t -> ch ) ) )
13	10 11 12	3bitr4g	|- ( ph -> ( [ z / x ] ps <-> [ w / y ] ch ) )