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