Theorem cbvcsbw

Description: Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on A . Version of cbvcsb with a disjoint variable condition, which does not require ax-13 . (Contributed by Jeff Hankins, 13-Sep-2009) (Revised by Gino Giotto, 10-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvcsbw.1	|- F/_ y C
2		cbvcsbw.2	|- F/_ x D
3		cbvcsbw.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	cbvsbcw	|- ( [. 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