Theorem elmapfn

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

	Ref	Expression
Assertion	elmapfn	⊢ ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) → 𝐴 Fn 𝐶 )

Proof

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