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	$$⊢\underset{\_}{Ⅎ}yC$$
	cbvcsb.2	$$⊢\underset{\_}{Ⅎ}xD$$
	cbvcsb.3	$$⊢x=y\to C=D$$
Assertion	cbvcsb	$$⊢⦋A/x⦌C=⦋A/y⦌D$$

Proof

Step	Hyp	Ref	Expression
1		cbvcsb.1	$$⊢\underset{\_}{Ⅎ}yC$$
2		cbvcsb.2	$$⊢\underset{\_}{Ⅎ}xD$$
3		cbvcsb.3	$$⊢x=y\to C=D$$
4	1	nfcri	$$⊢Ⅎyz\in C$$
5	2	nfcri	$$⊢Ⅎxz\in D$$
6	3	eleq2d	$$⊢x=y\to \left(z\in C\leftrightarrow z\in D\right)$$
7	4 5 6	cbvsbc	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in C\leftrightarrow \underset{\dot{}}{[}A/y\underset{\dot{}}{]}z\in D$$
8	7	abbii	$$⊢\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in C\right\}=\left\{z|\underset{\dot{}}{[}A/y\underset{\dot{}}{]}z\in D\right\}$$
9		df-csb	$$⊢⦋A/x⦌C=\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in C\right\}$$
10		df-csb	$$⊢⦋A/y⦌D=\left\{z|\underset{\dot{}}{[}A/y\underset{\dot{}}{]}z\in D\right\}$$
11	8 9 10	3eqtr4i	$$⊢⦋A/x⦌C=⦋A/y⦌D$$