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  7429  omp1eomlem  7435  ctm  7450  exmidfodomrlemim  7554  fcdmnn0fsuppg  9623  nn0supp  9624  frecuzrdg0  10864  frecuzrdgsuc  10865  frecuzrdgdomlem  10868  frecuzrdg0t  10873  frecuzrdgsuctlem  10874  climdm  12079  sum0  12173  isumz  12174  fsumsersdc  12180  isumclim  12206  zprodap0  12366  psrbaglesuppg  15108  iscnp3  15356  cnpnei  15372  cnclima  15376  cnrest2  15389  hmeores  15468  metcnp  15665  qtopbasss  15674  tgqioo  15708  dvaddxx  15856  dvmulxx  15857  dviaddf  15858  dvimulf  15859  dvef  15880  pilem3  15937  subusgr  16638  upgr2wlkdc  16740