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 )