Theorem cbvcsbdavw2

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

	Ref	Expression
Hypotheses	cbvcsbdavw2.1	|- ( ph -> A = B )
	cbvcsbdavw2.2	|- ( ( ph /\ x = y ) -> C = D )
Assertion	cbvcsbdavw2	|- ( ph -> [_ A / x ]_ C = [_ B / y ]_ D )

Proof

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