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 6555  ⟶wf 6557

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 6564  df-f 6565

This theorem is referenced by:  fofun  6821  fssrescdmd  7146  fmptco  7149  funfvima2d  7252  smores2  8394  elmapfun  8906  fidmfisupp  9412  fdmfifsupp  9415  fsuppmptif  9439  fsuppco2  9443  fsuppcor  9444  ordtypelem8  9565  ordtypelem9  9566  ordtypelem10  9567  unxpwdom2  9628  fpwwe2  10683  swrdwrdsymb  14700  mrcuni  17664  frmdss2  18876  cntzmhm2  19360  frgpupval  19792  gsumzadd  19940  gsumpt  19980  gsum2dlem2  19989  dprd2da  20062  lmhmpreima  21047  lmhmlsp  21048  rhmpreimaidl  21287  cygznlem2  21587  frlmsslsp  21816  frlmup1  21818  frlmup4  21821  lindff1  21840  lindfrn  21841  psrelbasfun  21955  mvrcl  22012  evlslem3  22104  evlseu  22107  mpfind  22131  mhpmulcl  22153  psdmul  22170  gsumply1subr  22235  cnclsi  23280  cncnp  23288  paste  23302  connima  23433  1stcfb  23453  1stccnp  23470  1stckgenlem  23561  txcnpi  23616  txcnp  23628  xkoco2cn  23666  fmfnfmlem2  23963  lmflf  24013  txflf  24014  cnextcn  24075  clssubg  24117  ghmcnp  24123  metustid  24567  metustexhalf  24569  isngp2  24610  pi1xfrval  25087  pi1coval  25093  iscfil2  25300  rrxcph  25426  ismbfd  25674  ellimc2  25912  ellimc3  25914  dvres3  25948  dvres3a  25949  dvcnv  26015  dvcnvrelem1  26056  ftc1cn  26084  mdegldg  26105  plyeq0  26250  plyaddlem1  26252  plymullem1  26253  ulmdv  26446  dchrelbas2  27281  dchrghm  27300  uhgrfun  29083  vdegp1ai  29554  vdegp1bi  29555  wlkres  29688  sspg  30747  ssps  30749  sspn  30755  htthlem  30936  fmptcof2  32667  fnpreimac  32681  curry2ima  32718  offinsupp1  32738  fpwrelmapffslem  32743  swrdrn2  32939  pwrssmgc  32990  gsumhashmul  33064  xrge0tsmsd  33065  wrdpmtrlast  33113  cyc3co2  33160  tocyccntz  33164  rmfsupp2  33242  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem3  33248  elrgspnlem4  33249  elrgspnsubrunlem1  33251  elrgspnsubrunlem2  33252  elrspunidl  33456  rhmimaidl  33460  ig1pmindeg  33622  ply1degltdimlem  33673  lbsdiflsp0  33677  fedgmullem1  33680  fedgmullem2  33681  evls1fldgencl  33720  fldextrspunlsp  33724  rhmpreimacnlem  33883  esumpfinvallem  34075  sibfof  34342  sitgclg  34344  eulerpartlemd  34368  eulerpartlemgu  34379  eulerpartlemgf  34381  dstrvprob  34474  dstfrvel  34476  orvclteinc  34478  spthcycl  35134  cvmliftmolem1  35286  cvmliftlem3  35292  cvmliftlem10  35299  cvmliftlem13  35301  cvmlift2lem9  35316  cvmlift3lem6  35329  cvmlift3lem7  35330  satefvfmla0  35423  satefvfmla1  35430  msubrn  35534  mclsax  35574  mclsppslem  35588  mclspps  35589  weiunfr  36468  ftc1cnnc  37699  heibor1lem  37816  grpokerinj  37900  aks6d1c3  42124  aks6d1c4  42125  sticksstones1  42147  aks6d1c6lem2  42172  rhmqusspan  42186  aks5lem2  42188  imacrhmcl  42524  evlsvvvallem  42571  evlselvlem  42596  evlselv  42597  lmhmfgima  43096  cantnfub  43334  onnog  43442  gneispacefun  44150  relpfrlem  44974  cncmpmax  45037  limccog  45635  limsuppnfdlem  45716  climxrrelem  45764  climxrre  45765  liminfvalxr  45798  liminflimsupxrre  45832  xlimxrre  45846  dvsinax  45928  fvvolioof  46004  fvvolicof  46006  dirkercncflem2  46119  fourierdlem82  46203  subsaliuncllem  46372  fge0iccico  46385  sge0sn  46394  sge0tsms  46395  sge0cl  46396  sge0f1o  46397  sge0isum  46442  ovnovollem1  46671  ovnovollem2  46672  preimaioomnf  46734  smfresal  46803  smfres  46805  smfco  46817  fcoreslem1  47075  fcoreslem2  47076  fcores  47079  gricushgr  47886  ushggricedg  47896  uspgrlimlem4  47958  cnneiima  48814  sepfsepc  48825