Description: A restriction to an image. (Contributed by NM, 29-Sep-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | resima | ⊢ ( ( 𝐴 ↾ 𝐵 ) “ 𝐵 ) = ( 𝐴 “ 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | residm | ⊢ ( ( 𝐴 ↾ 𝐵 ) ↾ 𝐵 ) = ( 𝐴 ↾ 𝐵 ) | |
2 | 1 | rneqi | ⊢ ran ( ( 𝐴 ↾ 𝐵 ) ↾ 𝐵 ) = ran ( 𝐴 ↾ 𝐵 ) |
3 | df-ima | ⊢ ( ( 𝐴 ↾ 𝐵 ) “ 𝐵 ) = ran ( ( 𝐴 ↾ 𝐵 ) ↾ 𝐵 ) | |
4 | df-ima | ⊢ ( 𝐴 “ 𝐵 ) = ran ( 𝐴 ↾ 𝐵 ) | |
5 | 2 3 4 | 3eqtr4i | ⊢ ( ( 𝐴 ↾ 𝐵 ) “ 𝐵 ) = ( 𝐴 “ 𝐵 ) |