Theorem ffun 5536

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 5533	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfun 5478	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)

This proof depends on syntax axioms:   → wi 4  Fun wfun 5371   Fn wfn 5372  ⟶wf 5373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-fn 5380  df-f 5381

This theorem is used by:  ffund  5537  funssxp  5557  f00  5584  fofun  5616  fun11iun  5660  fimacnv  5837  dff3im  5853  resflem  5872  fmptco  5874  fliftf  6005  fsuppeq  6487  fsuppeqg  6488  smores2  6565  pmfun  6942  elmapfun  6953  pmresg  6957  ac6sfi  7202  ffsuppbi  7300  casef  7428  omp1eomlem  7434  ctm  7449  exmidfodomrlemim  7553  fcdmnn0fsuppg  9620  nn0supp  9621  frecuzrdg0  10852  frecuzrdgsuc  10853  frecuzrdgdomlem  10856  frecuzrdg0t  10861  frecuzrdgsuctlem  10862  climdm  12063  sum0  12157  isumz  12158  fsumsersdc  12164  isumclim  12190  zprodap0  12350  psrbaglesuppg  15059  iscnp3  15306  cnpnei  15322  cnclima  15326  cnrest2  15339  hmeores  15418  metcnp  15615  qtopbasss  15624  tgqioo  15658  dvaddxx  15806  dvmulxx  15807  dviaddf  15808  dvimulf  15809  dvef  15830  pilem3  15887  subusgr  16528  upgr2wlkdc  16630