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

Metamath Proof Explorer

Theorem ffun

Description: A mapping is a function. (Contributed by NM, 3-Aug-1994)

Ref Expression
Assertion ffun ( 𝐹 : 𝐴 ⟶ 𝐵 → Fun 𝐹 )

Proof

Step Hyp Ref Expression
1 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
2 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
3 1 2 syl ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → Fun 𝐹 )