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	⊢ Ⅎ 𝑦 𝐶
	cbvcsbw.2	⊢ Ⅎ 𝑥 𝐷
	cbvcsbw.3	⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐷 )
Assertion	cbvcsbw	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑦 ⦌ 𝐷

Proof

Step	Hyp	Ref	Expression
1		cbvcsbw.1	⊢ Ⅎ 𝑦 𝐶
2		cbvcsbw.2	⊢ Ⅎ 𝑥 𝐷
3		cbvcsbw.3	⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐷 )
4	1	nfcri	⊢ Ⅎ 𝑦 𝑧 ∈ 𝐶
5	2	nfcri	⊢ Ⅎ 𝑥 𝑧 ∈ 𝐷
6	3	eleq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝐶 ↔ 𝑧 ∈ 𝐷 ) )
7	4 5 6	cbvsbcw	⊢ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐶 ↔ [ 𝐴 / 𝑦 ] 𝑧 ∈ 𝐷 )
8	7	abbii	⊢ { 𝑧 ∣ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐶 } = { 𝑧 ∣ [ 𝐴 / 𝑦 ] 𝑧 ∈ 𝐷 }
9		df-csb	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = { 𝑧 ∣ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐶 }
10		df-csb	⊢ ⦋ 𝐴 / 𝑦 ⦌ 𝐷 = { 𝑧 ∣ [ 𝐴 / 𝑦 ] 𝑧 ∈ 𝐷 }
11	8 9 10	3eqtr4i	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑦 ⦌ 𝐷

Metamath Proof Explorer

Theorem cbvcsbw

Proof