Theorem ffund 6740

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

Syntax hints:   → wi 4  Fun wfun 6556  ⟶wf 6558

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 207  df-an 396  df-fn 6565  df-f 6566

This theorem is referenced by:  fofun  6821  fssrescdmd  7145  fmptco  7148  funfvima2d  7251  smores2  8392  elmapfun  8904  fidmfisupp  9409  fdmfifsupp  9412  fsuppmptif  9436  fsuppco2  9440  fsuppcor  9441  ordtypelem8  9562  ordtypelem9  9563  ordtypelem10  9564  unxpwdom2  9625  fpwwe2  10680  swrdwrdsymb  14696  mrcuni  17665  frmdss2  18888  cntzmhm2  19372  frgpupval  19806  gsumzadd  19954  gsumpt  19994  gsum2dlem2  20003  dprd2da  20076  lmhmpreima  21064  lmhmlsp  21065  rhmpreimaidl  21304  cygznlem2  21604  frlmsslsp  21833  frlmup1  21835  frlmup4  21838  lindff1  21857  lindfrn  21858  psrelbasfun  21972  mvrcl  22029  evlslem3  22121  evlseu  22124  mpfind  22148  mhpmulcl  22170  psdmul  22187  gsumply1subr  22250  cnclsi  23295  cncnp  23303  paste  23317  connima  23448  1stcfb  23468  1stccnp  23485  1stckgenlem  23576  txcnpi  23631  txcnp  23643  xkoco2cn  23681  fmfnfmlem2  23978  lmflf  24028  txflf  24029  cnextcn  24090  clssubg  24132  ghmcnp  24138  metustid  24582  metustexhalf  24584  isngp2  24625  pi1xfrval  25100  pi1coval  25106  iscfil2  25313  rrxcph  25439  ismbfd  25687  ellimc2  25926  ellimc3  25928  dvres3  25962  dvres3a  25963  dvcnv  26029  dvcnvrelem1  26070  ftc1cn  26098  mdegldg  26119  plyeq0  26264  plyaddlem1  26266  plymullem1  26267  ulmdv  26460  dchrelbas2  27295  dchrghm  27314  uhgrfun  29097  vdegp1ai  29568  vdegp1bi  29569  wlkres  29702  sspg  30756  ssps  30758  sspn  30764  htthlem  30945  fmptcof2  32673  fnpreimac  32687  curry2ima  32723  offinsupp1  32744  fpwrelmapffslem  32749  swrdrn2  32923  pwrssmgc  32974  gsumhashmul  33046  xrge0tsmsd  33047  wrdpmtrlast  33095  cyc3co2  33142  tocyccntz  33146  rmfsupp2  33227  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem3  33233  elrgspnlem4  33234  elrspunidl  33435  rhmimaidl  33439  ig1pmindeg  33601  ply1degltdimlem  33649  lbsdiflsp0  33653  fedgmullem1  33656  fedgmullem2  33657  evls1fldgencl  33694  rhmpreimacnlem  33844  esumpfinvallem  34054  sibfof  34321  sitgclg  34323  eulerpartlemd  34347  eulerpartlemgu  34358  eulerpartlemgf  34360  dstrvprob  34452  dstfrvel  34454  orvclteinc  34456  spthcycl  35113  cvmliftmolem1  35265  cvmliftlem3  35271  cvmliftlem10  35278  cvmliftlem13  35280  cvmlift2lem9  35295  cvmlift3lem6  35308  cvmlift3lem7  35309  satefvfmla0  35402  satefvfmla1  35409  msubrn  35513  mclsax  35553  mclsppslem  35567  mclspps  35568  weiunfr  36449  ftc1cnnc  37678  heibor1lem  37795  grpokerinj  37879  aks6d1c3  42104  aks6d1c4  42105  sticksstones1  42127  aks6d1c6lem2  42152  rhmqusspan  42166  aks5lem2  42168  imacrhmcl  42500  evlsvvvallem  42547  evlselvlem  42572  evlselv  42573  lmhmfgima  43072  cantnfub  43310  onnog  43418  gneispacefun  44126  cncmpmax  44969  limccog  45575  limsuppnfdlem  45656  climxrrelem  45704  climxrre  45705  liminfvalxr  45738  liminflimsupxrre  45772  xlimxrre  45786  dvsinax  45868  fvvolioof  45944  fvvolicof  45946  dirkercncflem2  46059  fourierdlem82  46143  subsaliuncllem  46312  fge0iccico  46325  sge0sn  46334  sge0tsms  46335  sge0cl  46336  sge0f1o  46337  sge0isum  46382  ovnovollem1  46611  ovnovollem2  46612  preimaioomnf  46674  smfresal  46743  smfres  46745  smfco  46757  fcoreslem1  47012  fcoreslem2  47013  fcores  47016  gricushgr  47823  ushggricedg  47833  uspgrlimlem4  47893  cnneiima  48712  sepfsepc  48723