This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eceq2

Description: Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995)

Ref Expression
Assertion eceq2 ⊢ A = B → C A = C B

Proof

Step Hyp Ref Expression
1 imaeq1 ⊢ A = B → A C = B C
2 df-ec ⊢ C A = A C
3 df-ec ⊢ C B = B C
4 1 2 3 3eqtr4g ⊢ A = B → C A = C B