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

Ref | Expression | ||
---|---|---|---|

Assertion | imaeq2 | ⊢ ( 𝐴 = 𝐵 → ( 𝐶 “ 𝐴 ) = ( 𝐶 “ 𝐵 ) ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | reseq2 | ⊢ ( 𝐴 = 𝐵 → ( 𝐶 ↾ 𝐴 ) = ( 𝐶 ↾ 𝐵 ) ) | |

2 | 1 | rneqd | ⊢ ( 𝐴 = 𝐵 → ran ( 𝐶 ↾ 𝐴 ) = ran ( 𝐶 ↾ 𝐵 ) ) |

3 | df-ima | ⊢ ( 𝐶 “ 𝐴 ) = ran ( 𝐶 ↾ 𝐴 ) | |

4 | df-ima | ⊢ ( 𝐶 “ 𝐵 ) = ran ( 𝐶 ↾ 𝐵 ) | |

5 | 2 3 4 | 3eqtr4g | ⊢ ( 𝐴 = 𝐵 → ( 𝐶 “ 𝐴 ) = ( 𝐶 “ 𝐵 ) ) |