Theorem cbvcsbdavw

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

	Ref	Expression
Hypothesis	cbvcsbdavw.1	|- ( ( ph /\ x = y ) -> B = C )
Assertion	cbvcsbdavw	|- ( ph -> [_ A / x ]_ B = [_ A / y ]_ C )

Proof

Step	Hyp	Ref	Expression
1		cbvcsbdavw.1	|- ( ( ph /\ x = y ) -> B = C )
2	1	eleq2d	|- ( ( ph /\ x = y ) -> ( t e. B <-> t e. C ) )
3	2	cbvsbcdavw	|- ( ph -> ( [. A / x ]. t e. B <-> [. A / y ]. t e. C ) )
4	3	abbidv	|- ( ph -> { t | [. A / x ]. t e. B } = { t | [. A / y ]. t e. C } )
5		df-csb	|- [_ A / x ]_ B = { t | [. A / x ]. t e. B }
6		df-csb	|- [_ A / y ]_ C = { t | [. A / y ]. t e. C }
7	4 5 6	3eqtr4g	|- ( ph -> [_ A / x ]_ B = [_ A / y ]_ C )