Description: A restriction by an arbitrary set is a restriction by its domain. (Contributed by AV, 16-Nov-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | resresdm | |- ( F = ( E |` A ) -> F = ( E |` dom F ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | |- ( F = ( E |` A ) -> F = ( E |` A ) ) |
|
2 | dmeq | |- ( F = ( E |` A ) -> dom F = dom ( E |` A ) ) |
|
3 | 2 | reseq2d | |- ( F = ( E |` A ) -> ( E |` dom F ) = ( E |` dom ( E |` A ) ) ) |
4 | resdmres | |- ( E |` dom ( E |` A ) ) = ( E |` A ) |
|
5 | 3 4 | eqtr2di | |- ( F = ( E |` A ) -> ( E |` A ) = ( E |` dom F ) ) |
6 | 1 5 | eqtrd | |- ( F = ( E |` A ) -> F = ( E |` dom F ) ) |