Description: Equality deduction for substitution in class. (Contributed by Giovanni Mascellani, 10-Apr-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | csbeq12 | ⊢ ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥 𝐶 = 𝐷 ) → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑥 ⦌ 𝐷 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbeq2 | ⊢ ( ∀ 𝑥 𝐶 = 𝐷 → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) | |
2 | csbeq1 | ⊢ ( 𝐴 = 𝐵 → ⦋ 𝐴 / 𝑥 ⦌ 𝐷 = ⦋ 𝐵 / 𝑥 ⦌ 𝐷 ) | |
3 | 1 2 | sylan9eqr | ⊢ ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥 𝐶 = 𝐷 ) → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑥 ⦌ 𝐷 ) |