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

Metamath Proof Explorer

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 𝐴 )