**Description:** The image of the domain of a restriction. (Contributed by NM, 8-Apr-2007)

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

Assertion | imadmres | ⊢ ( 𝐴 “ dom ( 𝐴 ↾ 𝐵 ) ) = ( 𝐴 “ 𝐵 ) |

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

1 | resdmres | ⊢ ( 𝐴 ↾ dom ( 𝐴 ↾ 𝐵 ) ) = ( 𝐴 ↾ 𝐵 ) | |

2 | 1 | rneqi | ⊢ ran ( 𝐴 ↾ dom ( 𝐴 ↾ 𝐵 ) ) = ran ( 𝐴 ↾ 𝐵 ) |

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

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

5 | 2 3 4 | 3eqtr4i | ⊢ ( 𝐴 “ dom ( 𝐴 ↾ 𝐵 ) ) = ( 𝐴 “ 𝐵 ) |