Metamath Proof Explorer

Theorem imaeq2

Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994)

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

Proof

Step Hyp Ref Expression
1 reseq2 ⊢ A = B → C ↾ A = C ↾ B
2 1 rneqd ⊢ A = B → ran ⁡ C ↾ A = ran ⁡ C ↾ B
3 df-ima ⊢ C A = ran ⁡ C ↾ A
4 df-ima ⊢ C B = ran ⁡ C ↾ B
5 2 3 4 3eqtr4g ⊢ A = B → C A = C B