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		resindm	|- ( F |` ( C i^i dom F ) ) = ( F |` C )
6	4 5	eqtrdi	|- ( F : A --> B -> ( F |` ( C i^i A ) ) = ( F |` C ) )