Theorem feqresmpt

Description: Express a restricted function as a mapping. (Contributed by Mario Carneiro, 18-May-2016)

	Ref	Expression
Hypotheses	feqmptd.1	|- ( ph -> F : A --> B )
	feqresmpt.2	|- ( ph -> C C_ A )
Assertion	feqresmpt	|- ( ph -> ( F |` C ) = ( x e. C |-> ( F ` x ) ) )

Proof

Step	Hyp	Ref	Expression
1		feqmptd.1	|- ( ph -> F : A --> B )
2		feqresmpt.2	|- ( ph -> C C_ A )
3	1 2	fssresd	|- ( ph -> ( F |` C ) : C --> B )
4	3	feqmptd	|- ( ph -> ( F |` C ) = ( x e. C |-> ( ( F |` C ) ` x ) ) )
5		fvres	|- ( x e. C -> ( ( F |` C ) ` x ) = ( F ` x ) )
6	5	mpteq2ia	|- ( x e. C |-> ( ( F |` C ) ` x ) ) = ( x e. C |-> ( F ` x ) )
7	4 6	eqtrdi	|- ( ph -> ( F |` C ) = ( x e. C |-> ( F ` x ) ) )