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

Proof

Step	Hyp	Ref	Expression
1		cbvcsbw.1	$⊢ \underline{Ⅎ} y C$
2		cbvcsbw.2	$⊢ \underline{Ⅎ} x D$
3		cbvcsbw.3	$⊢ x = y \to C = D$
4	1	nfcri	$⊢ Ⅎ y z \in C$
5	2	nfcri	$⊢ Ⅎ x z \in D$
6	3	eleq2d	$⊢ x = y \to (z \in C \leftrightarrow z \in D)$
7	4 5 6	cbvsbcw	$⊢ \underset{˙}{[} A / x \underset{˙}{]} z \in C \leftrightarrow \underset{˙}{[} A / y \underset{˙}{]} z \in D$
8	7	abbii	$⊢ \{z \| \underset{˙}{[} A / x \underset{˙}{]} z \in C\} = \{z \| \underset{˙}{[} A / y \underset{˙}{]} z \in D\}$
9		df-csb	$⊢ ⦋ A / x ⦌ C = \{z \| \underset{˙}{[} A / x \underset{˙}{]} z \in C\}$
10		df-csb	$⊢ ⦋ A / y ⦌ D = \{z \| \underset{˙}{[} A / y \underset{˙}{]} z \in D\}$
11	8 9 10	3eqtr4i	$⊢ ⦋ A / x ⦌ C = ⦋ A / y ⦌ D$

Metamath Proof Explorer

Theorem cbvcsbw

Proof