Metamath Proof Explorer

Theorem elmapfun

Description: A mapping is always a function. (Contributed by Stefan O'Rear, 9-Oct-2014) (Revised by Stefan O'Rear, 5-May-2015)

Ref Expression
Assertion elmapfun 
|- ( A e. ( B ^m C ) -> Fun A )

Proof

Step Hyp Ref Expression
1 elmapi 
 |-  ( A e. ( B ^m C ) -> A : C --> B )
2 1 ffund 
 |-  ( A e. ( B ^m C ) -> Fun A )