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	$$⊢\phi \to B=C$$
Assertion	csbeq2dv	$$⊢\phi \to ⦋A/x⦌B=⦋A/x⦌C$$

Proof

Step	Hyp	Ref	Expression
1		csbeq2dv.1	$$⊢\phi \to B=C$$
2		nfv	$$⊢Ⅎx\phi$$
3	2 1	csbeq2d	$$⊢\phi \to ⦋A/x⦌B=⦋A/x⦌C$$