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