Theorem ffun 5539

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

This proof depends on syntax axioms:   → wi 4  Fun wfun 5374   Fn wfn 5375  ⟶wf 5376

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 5383  df-f 5384

This theorem is used by:  ffund  5540  funssxp  5560  f00  5587  fofun  5619  fun11iun  5663  fimacnv  5840  dff3im  5856  resflem  5875  fmptco  5877  fliftf  6008  fsuppeq  6491  fsuppeqg  6492  smores2  6569  pmfun  6946  elmapfun  6957  pmresg  6961  ac6sfi  7207  ffsuppbi  7306  casef  7435  omp1eomlem  7441  ctm  7456  exmidfodomrlemim  7560  fcdmnn0fsuppg  9630  nn0supp  9631  frecuzrdg0  10872  frecuzrdgsuc  10873  frecuzrdgdomlem  10876  frecuzrdg0t  10881  frecuzrdgsuctlem  10882  climdm  12087  sum0  12181  isumz  12182  fsumsersdc  12188  isumclim  12214  zprodap0  12374  psrbaglesuppg  15172  iscnp3  15441  cnpnei  15457  cnclima  15461  cnrest2  15474  hmeores  15553  metcnp  15750  qtopbasss  15759  tgqioo  15793  dvaddxx  15941  dvmulxx  15942  dviaddf  15943  dvimulf  15944  dvef  15965  pilem3  16022  subusgr  16733  upgr2wlkdc  16835