Metamath Proof Explorer


Theorem curry2f

Description: Functionality of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008)

Ref Expression
Hypothesis curry2.1 G=F1stV×C-1
Assertion curry2f F:A×BDCBG:AD

Proof

Step Hyp Ref Expression
1 curry2.1 G=F1stV×C-1
2 ffn F:A×BDFFnA×B
3 1 curry2 FFnA×BCBG=xAxFC
4 2 3 sylan F:A×BDCBG=xAxFC
5 fovcdm F:A×BDxACBxFCD
6 5 3com23 F:A×BDCBxAxFCD
7 6 3expa F:A×BDCBxAxFCD
8 4 7 fmpt3d F:A×BDCBG:AD