Theorem cbvsbdavw

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

	Ref	Expression
Hypothesis	cbvsbdavw.1	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
Assertion	cbvsbdavw	|- ( ph -> ( [ z / x ] ps <-> [ z / y ] ch ) )

Proof

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