Metamath Proof Explorer


Theorem feqresmptf

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

Ref Expression
Hypotheses feqresmptf.1 _ x F
feqresmptf.2 φ F : A B
feqresmptf.3 φ C A
Assertion feqresmptf φ F C = x C F x

Proof

Step Hyp Ref Expression
1 feqresmptf.1 _ x F
2 feqresmptf.2 φ F : A B
3 feqresmptf.3 φ C A
4 nfcv _ x C
5 1 4 nfres _ x F C
6 2 3 fssresd φ F C : C B
7 4 5 6 feqmptdf φ F C = x C F C x
8 fvres x C F C x = F x
9 8 mpteq2ia x C F C x = x C F x
10 7 9 eqtrdi φ F C = x C F x