Theorem csbeq2i

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

	Ref	Expression
Hypothesis	csbeq2i.1	⊢ 𝐵 = 𝐶
Assertion	csbeq2i	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶

Proof

Step	Hyp	Ref	Expression
1		csbeq2i.1	⊢ 𝐵 = 𝐶
2	1	a1i	⊢ ( ⊤ → 𝐵 = 𝐶 )
3	2	csbeq2dv	⊢ ( ⊤ → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
4	3	mptru	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶