Theorem feqresmptf

Description: Express a restricted function as a mapping. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	feqresmptf.1	|- F/_ x F
	feqresmptf.2	|- ( ph -> F : A --> B )
	feqresmptf.3	|- ( ph -> C C_ A )
Assertion	feqresmptf	|- ( ph -> ( F |` C ) = ( x e. C |-> ( F ` x ) ) )

Proof

Step	Hyp	Ref	Expression
1		feqresmptf.1	|- F/_ x F
2		feqresmptf.2	|- ( ph -> F : A --> B )
3		feqresmptf.3	|- ( ph -> C C_ A )
4		nfcv	|- F/_ x C
5	1 4	nfres	|- F/_ x ( F |` C )
6	2 3	fssresd	|- ( ph -> ( F |` C ) : C --> B )
7	4 5 6	feqmptdf	|- ( ph -> ( F |` C ) = ( x e. C |-> ( ( F |` C ) ` x ) ) )
8		fvres	|- ( x e. C -> ( ( F |` C ) ` x ) = ( F ` x ) )
9	8	mpteq2ia	|- ( x e. C |-> ( ( F |` C ) ` x ) ) = ( x e. C |-> ( F ` x ) )
10	7 9	eqtrdi	|- ( ph -> ( F |` C ) = ( x e. C |-> ( F ` x ) ) )