Theorem ffund 6588

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 6587	. 2 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)
3	1, 2	syl 17	1 ⊢ (𝜑 → Fun 𝐹)

Syntax hints:   → wi 4  Fun wfun 6412  ⟶wf 6414

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 206  df-an 396  df-fn 6421  df-f 6422

This theorem is referenced by:  fofun  6673  fmptco  6983  funfvima2d  7090  smores2  8156  elmapfun  8612  fdmfifsupp  9068  fsuppmptif  9088  fsuppco2  9092  fsuppcor  9093  ordtypelem8  9214  ordtypelem9  9215  ordtypelem10  9216  unxpwdom2  9277  fpwwe2  10330  swrdwrdsymb  14303  mrcuni  17247  frmdss2  18417  cntzmhm2  18861  frgpupval  19295  gsumzadd  19438  gsumpt  19478  gsum2dlem2  19487  dprd2da  19560  lmhmpreima  20225  lmhmlsp  20226  cygznlem2  20688  frlmsslsp  20913  frlmup1  20915  frlmup4  20918  lindff1  20937  lindfrn  20938  psrelbasfun  21059  mvrcl  21131  evlslem3  21200  evlseu  21203  mpfind  21227  mhpmulcl  21249  gsumply1subr  21315  cnclsi  22331  cncnp  22339  paste  22353  connima  22484  1stcfb  22504  1stccnp  22521  1stckgenlem  22612  txcnpi  22667  txcnp  22679  xkoco2cn  22717  fmfnfmlem2  23014  lmflf  23064  txflf  23065  cnextcn  23126  clssubg  23168  ghmcnp  23174  metustid  23616  metustexhalf  23618  isngp2  23659  pi1xfrval  24123  pi1coval  24129  iscfil2  24335  rrxcph  24461  ismbfd  24708  ellimc2  24946  ellimc3  24948  dvres3  24982  dvres3a  24983  dvcnv  25046  dvcnvrelem1  25086  ftc1cn  25112  mdegldg  25136  plyeq0  25277  plyaddlem1  25279  plymullem1  25280  ulmdv  25467  dchrelbas2  26290  dchrghm  26309  uhgrfun  27339  vdegp1ai  27806  vdegp1bi  27807  wlkres  27940  sspg  28991  ssps  28993  sspn  28999  htthlem  29180  fmptcof2  30896  fnpreimac  30910  curry2ima  30943  offinsupp1  30964  fpwrelmapffslem  30969  swrdrn2  31128  pwrssmgc  31180  gsumhashmul  31218  xrge0tsmsd  31219  cyc3co2  31309  tocyccntz  31313  rmfsupp2  31394  rhmpreimaidl  31505  elrspunidl  31508  rhmimaidl  31511  lbsdiflsp0  31609  fedgmullem1  31612  fedgmullem2  31613  rhmpreimacnlem  31736  esumpfinvallem  31942  sibfof  32207  sitgclg  32209  eulerpartlemd  32233  eulerpartlemgu  32244  eulerpartlemgf  32246  dstrvprob  32338  dstfrvel  32340  orvclteinc  32342  spthcycl  32991  cvmliftmolem1  33143  cvmliftlem3  33149  cvmliftlem10  33156  cvmliftlem13  33158  cvmlift2lem9  33173  cvmlift3lem6  33186  cvmlift3lem7  33187  satefvfmla0  33280  satefvfmla1  33287  msubrn  33391  mclsax  33431  mclsppslem  33445  mclspps  33446  ftc1cnnc  35776  heibor1lem  35894  grpokerinj  35978  sticksstones1  40030  lmhmfgima  40825  gneispacefun  41636  cncmpmax  42464  fidmfisupp  42628  limccog  43051  limsuppnfdlem  43132  climxrrelem  43180  climxrre  43181  liminfvalxr  43214  liminflimsupxrre  43248  xlimxrre  43262  dvsinax  43344  fvvolioof  43420  fvvolicof  43422  dirkercncflem2  43535  fourierdlem82  43619  subsaliuncllem  43786  fge0iccico  43798  sge0sn  43807  sge0tsms  43808  sge0cl  43809  sge0f1o  43810  sge0isum  43855  ovnovollem1  44084  ovnovollem2  44085  preimaioomnf  44143  smfresal  44209  smfres  44211  smfco  44223  fcoreslem1  44444  fcoreslem2  44445  fcores  44448  isomushgr  45166  ushrisomgr  45181  cnneiima  46098  sepfsepc  46109