Theorem ffund 6518

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

Syntax hints:   → wi 4  Fun wfun 6349  ⟶wf 6351

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 209  df-an 399  df-fn 6358  df-f 6359

This theorem is referenced by:  fofun  6591  fmptco  6891  funfvima2d  6994  smores2  7991  elmapfun  8430  fdmfifsupp  8843  fsuppmptif  8863  fsuppco2  8866  fsuppcor  8867  ordtypelem8  8989  ordtypelem9  8990  ordtypelem10  8991  unxpwdom2  9052  fpwwe2  10065  swrdwrdsymb  14024  mrcuni  16892  frmdss2  18028  cntzmhm2  18470  frgpupval  18900  gsumzadd  19042  gsumpt  19082  gsum2dlem2  19091  dprd2da  19164  lmhmpreima  19820  lmhmlsp  19821  psrelbasfun  20160  mvrcl  20229  evlslem3  20293  evlseu  20296  mpfind  20320  gsumply1subr  20402  cygznlem2  20715  frlmsslsp  20940  frlmup1  20942  frlmup4  20945  lindff1  20964  lindfrn  20965  cnclsi  21880  cncnp  21888  paste  21902  connima  22033  1stcfb  22053  1stccnp  22070  1stckgenlem  22161  txcnpi  22216  txcnp  22228  xkoco2cn  22266  fmfnfmlem2  22563  lmflf  22613  txflf  22614  cnextcn  22675  clssubg  22717  ghmcnp  22723  metustid  23164  metustexhalf  23166  isngp2  23206  pi1xfrval  23658  pi1coval  23664  iscfil2  23869  rrxcph  23995  ismbfd  24240  ellimc2  24475  ellimc3  24477  dvres3  24511  dvres3a  24512  dvcnv  24574  dvcnvrelem1  24614  ftc1cn  24640  mdegldg  24660  plyeq0  24801  plyaddlem1  24803  plymullem1  24804  ulmdv  24991  dchrelbas2  25813  dchrghm  25832  uhgrfun  26851  vdegp1ai  27318  vdegp1bi  27319  wlkres  27452  sspg  28505  ssps  28507  sspn  28513  htthlem  28694  fmptcof2  30402  fnpreimac  30416  curry2ima  30444  offinsupp1  30463  fpwrelmapffslem  30468  swrdrn2  30628  xrge0tsmsd  30692  cyc3co2  30782  tocyccntz  30786  rmfsupp2  30866  lbsdiflsp0  31022  fedgmullem1  31025  fedgmullem2  31026  esumpfinvallem  31333  sibfof  31598  sitgclg  31600  eulerpartlemd  31624  eulerpartlemgu  31635  eulerpartlemgf  31637  dstrvprob  31729  dstfrvel  31731  orvclteinc  31733  spthcycl  32376  cvmliftmolem1  32528  cvmliftlem3  32534  cvmliftlem10  32541  cvmliftlem13  32543  cvmlift2lem9  32558  cvmlift3lem6  32571  cvmlift3lem7  32572  satefvfmla0  32665  satefvfmla1  32672  msubrn  32776  mclsax  32816  mclsppslem  32830  mclspps  32831  ftc1cnnc  34981  heibor1lem  35102  grpokerinj  35186  lmhmfgima  39704  gneispacefun  40507  cncmpmax  41309  fidmfisupp  41482  limccog  41921  limsuppnfdlem  42002  climxrrelem  42050  climxrre  42051  liminfvalxr  42084  liminflimsupxrre  42118  xlimxrre  42132  dvsinax  42217  fvvolioof  42294  fvvolicof  42296  dirkercncflem2  42409  fourierdlem82  42493  subsaliuncllem  42660  fge0iccico  42672  sge0sn  42681  sge0tsms  42682  sge0cl  42683  sge0f1o  42684  sge0isum  42729  ovnovollem1  42958  ovnovollem2  42959  preimaioomnf  43017  smfresal  43083  smfres  43085  smfco  43097  isomushgr  44011  ushrisomgr  44026