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) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

	Ref	Expression
Hypotheses	cbvcsbw.1	$$⊢\underset{\_}{Ⅎ}yC$$
	cbvcsbw.2	$$⊢\underset{\_}{Ⅎ}xD$$
	cbvcsbw.3	$$⊢x=y\to C=D$$
Assertion	cbvcsbw	$$⊢⦋A/x⦌C=⦋A/y⦌D$$

Proof

Step	Hyp	Ref	Expression
1		cbvcsbw.1	$$⊢\underset{\_}{Ⅎ}yC$$
2		cbvcsbw.2	$$⊢\underset{\_}{Ⅎ}xD$$
3		cbvcsbw.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	cbvsbcw	$$⊢\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$$