Theorem cbvcsbv

Description: Change the bound variable of a proper substitution into a class using implicit substitution. (Contributed by NM, 30-Sep-2008) (Revised by Mario Carneiro, 13-Oct-2016)

	Ref	Expression
Hypothesis	cbvcsbv.1	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
Assertion	cbvcsbv	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑦 ⦌ 𝐶

Proof

Step	Hyp	Ref	Expression
1		cbvcsbv.1	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
2		nfcv	⊢ Ⅎ 𝑦 𝐵
3		nfcv	⊢ Ⅎ 𝑥 𝐶
4	2 3 1	cbvcsbw	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑦 ⦌ 𝐶