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	⊢ ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) → Fun 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elmapi	⊢ ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) → 𝐴 : 𝐶 ⟶ 𝐵 )
2	1	ffund	⊢ ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) → Fun 𝐴 )