Metamath Proof Explorer


Theorem fresin2

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 ) )

Proof

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 ) )