This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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