Theorem cbvcsbvw2

Description: Change bound variable of a proper substitution into a class using implicit substitution. General version of cbvcsbv . (Contributed by GG, 1-Sep-2025)

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

Proof

Step	Hyp	Ref	Expression
1		cbvcsbvw2.1	|- A = B
2		cbvcsbvw2.2	|- ( x = y -> C = D )
3	2	eleq2d	|- ( x = y -> ( t e. C <-> t e. D ) )
4	1 3	cbvsbcvw2	|- ( [. A / x ]. t e. C <-> [. B / y ]. t e. D )
5	4	abbii	|- { 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	3eqtr4i	|- [_ A / x ]_ C = [_ B / y ]_ D