Metamath Proof Explorer


Theorem csbeq12

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

Ref Expression
Assertion csbeq12 ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥 𝐶 = 𝐷 ) → 𝐴 / 𝑥 𝐶 = 𝐵 / 𝑥 𝐷 )

Proof

Step Hyp Ref Expression
1 csbeq2 ( ∀ 𝑥 𝐶 = 𝐷 𝐴 / 𝑥 𝐶 = 𝐴 / 𝑥 𝐷 )
2 csbeq1 ( 𝐴 = 𝐵 𝐴 / 𝑥 𝐷 = 𝐵 / 𝑥 𝐷 )
3 1 2 sylan9eqr ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥 𝐶 = 𝐷 ) → 𝐴 / 𝑥 𝐶 = 𝐵 / 𝑥 𝐷 )