Theorem elmapi

Description: A mapping is a function, forward direction only with superfluous antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014)

	Ref	Expression
Assertion	elmapi	|- ( A e. ( B ^m C ) -> A : C --> B )

Proof

Step	Hyp	Ref	Expression
1		elmapex	|- ( A e. ( B ^m C ) -> ( B e. _V /\ C e. _V ) )
2		elmapg	|- ( ( B e. _V /\ C e. _V ) -> ( A e. ( B ^m C ) <-> A : C --> B ) )
3	1 2	syl	|- ( A e. ( B ^m C ) -> ( A e. ( B ^m C ) <-> A : C --> B ) )
4	3	ibi	|- ( A e. ( B ^m C ) -> A : C --> B )