Theorem csbeq12

Description: Equality deduction for substitution in class. (Contributed by Giovanni Mascellani, 10-Apr-2018)

	Ref	Expression
Assertion	csbeq12	$$⊢\left(A=B\wedge \forall xC=D\right)\to ⦋A/x⦌C=⦋B/x⦌D$$

Proof

Step	Hyp	Ref	Expression
1		csbeq2	$$⊢\forall xC=D\to ⦋A/x⦌C=⦋A/x⦌D$$
2		csbeq1	$$⊢A=B\to ⦋A/x⦌D=⦋B/x⦌D$$
3	1 2	sylan9eqr	$$⊢\left(A=B\wedge \forall xC=D\right)\to ⦋A/x⦌C=⦋B/x⦌D$$