Theorem ffund 6666

Description: A mapping is a function, deduction version. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

Hypothesis

Ref	Expression
ffund.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
ffund	⊢ (𝜑 → Fun 𝐹)

Proof of Theorem ffund

Step	Hyp	Ref	Expression
1		ffund.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		ffun 6665	. 2 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)
3	1, 2	syl 17	1 ⊢ (𝜑 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 6486  ⟶wf 6488

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-fn 6495  df-f 6496

This theorem is referenced by:  fofun  6747  fssrescdmd  7075  fmptco  7078  funfvima2d  7183  smores2  8291  elmapfun  8810  fidmfisupp  9282  fdmfifsupp  9285  fsuppmptif  9309  fsuppco2  9313  fsuppcor  9314  ordtypelem8  9437  ordtypelem9  9438  ordtypelem10  9439  unxpwdom2  9500  fpwwe2  10564  swrdwrdsymb  14623  mrcuni  17585  frmdss2  18829  cntzmhm2  19315  frgpupval  19747  gsumzadd  19895  gsumpt  19935  gsum2dlem2  19944  dprd2da  20017  lmhmpreima  21045  lmhmlsp  21046  rhmpreimaidl  21277  cygznlem2  21550  frlmsslsp  21778  frlmup1  21780  frlmup4  21783  lindff1  21802  lindfrn  21803  psrelbasfun  21918  mvrcl  21973  evlslem3  22063  evlseu  22066  evlsvvvallem  22074  mpfind  22098  mhpmulcl  22144  psdmul  22161  gsumply1subr  22225  cnclsi  23262  cncnp  23270  paste  23284  connima  23415  1stcfb  23435  1stccnp  23452  1stckgenlem  23543  txcnpi  23598  txcnp  23610  xkoco2cn  23648  fmfnfmlem2  23945  lmflf  23995  txflf  23996  cnextcn  24057  clssubg  24099  ghmcnp  24105  metustid  24544  metustexhalf  24546  isngp2  24587  pi1xfrval  25046  pi1coval  25052  iscfil2  25258  rrxcph  25384  ismbfd  25631  ellimc2  25869  ellimc3  25871  dvres3  25905  dvres3a  25906  dvcnv  25969  dvcnvrelem1  26009  ftc1cn  26035  mdegldg  26056  plyeq0  26201  plyaddlem1  26203  plymullem1  26204  ulmdv  26393  dchrelbas2  27225  dchrghm  27244  uhgrfun  29160  vdegp1ai  29630  vdegp1bi  29631  wlkres  29762  sspg  30824  ssps  30826  sspn  30832  htthlem  31013  fmptcof2  32756  fnpreimac  32769  curry2ima  32808  offinsupp1  32825  fpwrelmapffslem  32831  indfsd  32954  swrdrn2  33040  pwrssmgc  33086  gsumhashmul  33155  xrge0tsmsd  33161  wrdpmtrlast  33181  cyc3co2  33228  tocyccntz  33232  rmfsupp2  33326  elrgspnlem1  33330  elrgspnlem2  33331  elrgspnlem3  33332  elrgspnlem4  33333  elrgspnsubrunlem1  33335  elrgspnsubrunlem2  33336  elrspunidl  33518  rhmimaidl  33522  ig1pmindeg  33692  selvascl  33708  extvfvcl  33727  mplmulmvr  33730  evlextv  33733  psrmonprod  33743  esplylem  33757  esplympl  33758  esplymhp  33759  esplyfv1  33760  ply1degltdimlem  33813  lbsdiflsp0  33817  fedgmullem1  33820  fedgmullem2  33821  evls1fldgencl  33861  fldextrspunlsp  33865  extdgfialglem1  33883  rhmpreimacnlem  34075  esumpfinvallem  34265  sibfof  34531  sitgclg  34533  eulerpartlemd  34557  eulerpartlemgu  34568  eulerpartlemgf  34570  dstrvprob  34663  dstfrvel  34665  orvclteinc  34667  spthcycl  35364  cvmliftmolem1  35516  cvmliftlem3  35522  cvmliftlem10  35529  cvmliftlem13  35531  cvmlift2lem9  35546  cvmlift3lem6  35559  cvmlift3lem7  35560  satefvfmla0  35653  satefvfmla1  35660  msubrn  35764  mclsax  35804  mclsppslem  35818  mclspps  35819  weiunfr  36702  ftc1cnnc  38066  heibor1lem  38183  grpokerinj  38267  aks6d1c3  42615  aks6d1c4  42616  sticksstones1  42638  aks6d1c6lem2  42663  rhmqusspan  42677  aks5lem2  42679  imacrhmcl  43011  evlselvlem  43045  evlselv  43046  lmhmfgima  43536  cantnfub  43773  onnoxpg  43880  gneispacefun  44588  relpfrlem  45404  cncmpmax  45487  limccog  46072  limsuppnfdlem  46151  climxrrelem  46199  climxrre  46200  liminfvalxr  46233  liminflimsupxrre  46267  xlimxrre  46281  dvsinax  46363  fvvolioof  46439  fvvolicof  46441  dirkercncflem2  46554  fourierdlem82  46638  subsaliuncllem  46807  fge0iccico  46820  sge0sn  46829  sge0tsms  46830  sge0cl  46831  sge0f1o  46832  sge0isum  46877  ovnovollem1  47106  ovnovollem2  47107  preimaioomnf  47169  smfresal  47238  smfres  47240  smfco  47252  fcoreslem1  47533  fcoreslem2  47534  fcores  47537  gricushgr  48415  ushggricedg  48425  uspgrlimlem4  48489  ffvbr  49353  cnneiima  49414  sepfsepc  49425  imaf1co  49652