Description: Restriction of a function with respect to the intersection with its domain. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | fresin2 | |- ( F : A --> B -> ( F |` ( C i^i A ) ) = ( F |` C ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fdm | |- ( F : A --> B -> dom F = A ) |
|
2 | 1 | eqcomd | |- ( F : A --> B -> A = dom F ) |
3 | 2 | ineq2d | |- ( F : A --> B -> ( C i^i A ) = ( C i^i dom F ) ) |
4 | 3 | reseq2d | |- ( F : A --> B -> ( F |` ( C i^i A ) ) = ( F |` ( C i^i dom F ) ) ) |
5 | frel | |- ( F : A --> B -> Rel F ) |
|
6 | resindm | |- ( Rel F -> ( F |` ( C i^i dom F ) ) = ( F |` C ) ) |
|
7 | 5 6 | syl | |- ( F : A --> B -> ( F |` ( C i^i dom F ) ) = ( F |` C ) ) |
8 | 4 7 | eqtrd | |- ( F : A --> B -> ( F |` ( C i^i A ) ) = ( F |` C ) ) |