Theorem csbeq2dv

Description: Formula-building deduction for class substitution. (Contributed by NM, 10-Nov-2005) (Revised by Mario Carneiro, 1-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		csbeq2dv.1	⊢ ( 𝜑 → 𝐵 = 𝐶 )
2		nfv	⊢ Ⅎ 𝑥 𝜑
3	2 1	csbeq2d	⊢ ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )