Theorem cbvcsbv

Description: Change the bound variable of a proper substitution into a class using implicit substitution. (Contributed by NM, 30-Sep-2008) (Revised by Mario Carneiro, 13-Oct-2016)

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

Proof

Step	Hyp	Ref	Expression
1		cbvcsbv.1	|- ( x = y -> B = C )
2	1	eleq2d	|- ( x = y -> ( z e. B <-> z e. C ) )
3	2	cbvsbcvw	|- ( [. A / x ]. z e. B <-> [. A / y ]. z e. C )
4	3	abbii	|- { z | [. A / x ]. z e. B } = { z | [. A / y ]. z e. C }
5		df-csb	|- [_ A / x ]_ B = { z | [. A / x ]. z e. B }
6		df-csb	|- [_ A / y ]_ C = { z | [. A / y ]. z e. C }
7	4 5 6	3eqtr4i	|- [_ A / x ]_ B = [_ A / y ]_ C