Theorem ffun 5406

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

Assertion

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

Proof of Theorem ffun

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

Syntax hints:   → wi 4  Fun wfun 5248   Fn wfn 5249  ⟶wf 5250

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-fn 5257  df-f 5258

This theorem is referenced by:  ffund  5407  funssxp  5423  f00  5445  fofun  5477  fun11iun  5521  fimacnv  5687  dff3im  5703  resflem  5722  fmptco  5724  fliftf  5842  smores2  6347  pmfun  6722  elmapfun  6726  pmresg  6730  ac6sfi  6954  casef  7147  omp1eomlem  7153  ctm  7168  exmidfodomrlemim  7261  nn0supp  9292  frecuzrdg0  10484  frecuzrdgsuc  10485  frecuzrdgdomlem  10488  frecuzrdg0t  10493  frecuzrdgsuctlem  10494  climdm  11438  sum0  11531  isumz  11532  fsumsersdc  11538  isumclim  11564  zprodap0  11724  psrbaglesuppg  14158  iscnp3  14371  cnpnei  14387  cnclima  14391  cnrest2  14404  hmeores  14483  metcnp  14680  qtopbasss  14689  tgqioo  14715  dvaddxx  14852  dvmulxx  14853  dviaddf  14854  dvimulf  14855  dvef  14873  pilem3  14918