Theorem cbvcsb

Description: Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on A . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvcsbw when possible. (Contributed by Jeff Hankins, 13-Sep-2009) (Revised by Mario Carneiro, 11-Dec-2016) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbvcsb.1	|- F/_ y C
2		cbvcsb.2	|- F/_ x D
3		cbvcsb.3	|- ( x = y -> C = D )
4	1	nfcri	|- F/ y z e. C
5	2	nfcri	|- F/ x z e. D
6	3	eleq2d	|- ( x = y -> ( z e. C <-> z e. D ) )
7	4 5 6	cbvsbc	|- ( [. A / x ]. z e. C <-> [. A / y ]. z e. D )
8	7	abbii	|- { z | [. A / x ]. z e. C } = { z | [. A / y ]. z e. D }
9		df-csb	|- [_ A / x ]_ C = { z | [. A / x ]. z e. C }
10		df-csb	|- [_ A / y ]_ D = { z | [. A / y ]. z e. D }
11	8 9 10	3eqtr4i	|- [_ A / x ]_ C = [_ A / y ]_ D