Metamath Proof Explorer

Theorem csbeq12

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

Ref Expression
Assertion csbeq12 
|- ( ( A = B /\ A. x C = D ) -> [_ A / x ]_ C = [_ B / x ]_ D )

Proof

Step Hyp Ref Expression
1 csbeq2 
 |-  ( A. x C = D -> [_ A / x ]_ C = [_ A / x ]_ D )
2 csbeq1 
 |-  ( A = B -> [_ A / x ]_ D = [_ B / x ]_ D )
3 1 2 sylan9eqr 
 |-  ( ( A = B /\ A. x C = D ) -> [_ A / x ]_ C = [_ B / x ]_ D )