Theorem curry1f

Description: Functionality of a curried function with a constant first argument. (Contributed by NM, 29-Mar-2008)

	Ref	Expression
Hypothesis	curry1.1	|- G = ( F o. `' ( 2nd |` ( { C } X. _V ) ) )
Assertion	curry1f	|- ( ( F : ( A X. B ) --> D /\ C e. A ) -> G : B --> D )

Proof

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