Theorem ffun 2754

Description: A mapping is a function.

Assertion

Ref	Expression
ffun	⊢ (F:A–→B → Fun F)

Proof of Theorem ffun

Step	Hyp	Ref	Expression
1		ffn 2752	. 2 ⊢ (F:A–→B → F Fn A)
2		fnfun 2721	. 2 ⊢ (F Fn A → Fun F)
3	1, 2	syl 12	1 ⊢ (F:A–→B → Fun F)

Syntax hints:   → wi 2  Fun wfun 2416   Fn wfn 2417  –→wf 2418

This theorem is referenced by:  fco 2760  f00 2773  fornex 2793  f1ores 2813  f1ococnv2 2817  cbvfo 2923  mapenlem1 3384  ac6lem 3575  fodom 3613  fodomb 3615  carduniima 3695  ruclem10 4894  ruclem11 4895  infxpidmlem7 4939  infmap2 4953  hoco 5598

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198  df-fn 2433  df-f 2434

metamath.org