Metamath Proof Explorer

Theorem elmapfn

Description: A mapping is a function with the appropriate domain. (Contributed by AV, 6-Apr-2019)

Ref Expression
Assertion elmapfn 
|- ( A e. ( B ^m C ) -> A Fn C )

Proof

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