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 = ( F o. `' ( 1st |` ( _V X. { C } ) ) )
Assertion	curry2f	|- ( ( F : ( A X. B ) --> D /\ C e. B ) -> G : A --> D )

Proof

Step	Hyp	Ref	Expression
1		curry2.1	|- G = ( F o. `' ( 1st |` ( _V X. { C } ) ) )
2		ffn	|- ( F : ( A X. B ) --> D -> F Fn ( A X. B ) )
3	1	curry2	|- ( ( F Fn ( A X. B ) /\ C e. B ) -> G = ( x e. A |-> ( x F C ) ) )
4	2 3	sylan	|- ( ( F : ( A X. B ) --> D /\ C e. B ) -> G = ( x e. A |-> ( x F C ) ) )
5		fovrn	|- ( ( F : ( A X. B ) --> D /\ x e. A /\ C e. B ) -> ( x F C ) e. D )
6	5	3com23	|- ( ( F : ( A X. B ) --> D /\ C e. B /\ x e. A ) -> ( x F C ) e. D )
7	6	3expa	|- ( ( ( F : ( A X. B ) --> D /\ C e. B ) /\ x e. A ) -> ( x F C ) e. D )
8	4 7	fmpt3d	|- ( ( F : ( A X. B ) --> D /\ C e. B ) -> G : A --> D )