Theorem ffund 6491

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

Syntax hints:   → wi 4  Fun wfun 6318  ⟶wf 6320

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 210  df-an 400  df-fn 6327  df-f 6328

This theorem is referenced by:  fofun  6566  fmptco  6868  funfvima2d  6972  smores2  7974  elmapfun  8413  fdmfifsupp  8827  fsuppmptif  8847  fsuppco2  8850  fsuppcor  8851  ordtypelem8  8973  ordtypelem9  8974  ordtypelem10  8975  unxpwdom2  9036  fpwwe2  10054  swrdwrdsymb  14015  mrcuni  16884  frmdss2  18020  cntzmhm2  18462  frgpupval  18892  gsumzadd  19035  gsumpt  19075  gsum2dlem2  19084  dprd2da  19157  lmhmpreima  19813  lmhmlsp  19814  cygznlem2  20260  frlmsslsp  20485  frlmup1  20487  frlmup4  20490  lindff1  20509  lindfrn  20510  psrelbasfun  20618  mvrcl  20688  evlslem3  20752  evlseu  20755  mpfind  20779  gsumply1subr  20863  cnclsi  21877  cncnp  21885  paste  21899  connima  22030  1stcfb  22050  1stccnp  22067  1stckgenlem  22158  txcnpi  22213  txcnp  22225  xkoco2cn  22263  fmfnfmlem2  22560  lmflf  22610  txflf  22611  cnextcn  22672  clssubg  22714  ghmcnp  22720  metustid  23161  metustexhalf  23163  isngp2  23203  pi1xfrval  23659  pi1coval  23665  iscfil2  23870  rrxcph  23996  ismbfd  24243  ellimc2  24480  ellimc3  24482  dvres3  24516  dvres3a  24517  dvcnv  24580  dvcnvrelem1  24620  ftc1cn  24646  mdegldg  24667  plyeq0  24808  plyaddlem1  24810  plymullem1  24811  ulmdv  24998  dchrelbas2  25821  dchrghm  25840  uhgrfun  26859  vdegp1ai  27326  vdegp1bi  27327  wlkres  27460  sspg  28511  ssps  28513  sspn  28519  htthlem  28700  fmptcof2  30420  fnpreimac  30434  curry2ima  30468  offinsupp1  30489  fpwrelmapffslem  30494  swrdrn2  30654  pwrssmgc  30706  gsumhashmul  30741  xrge0tsmsd  30742  cyc3co2  30832  tocyccntz  30836  rmfsupp2  30917  rhmpreimaidl  31011  elrspunidl  31014  rhmimaidl  31017  lbsdiflsp0  31110  fedgmullem1  31113  fedgmullem2  31114  rhmpreimacnlem  31237  esumpfinvallem  31443  sibfof  31708  sitgclg  31710  eulerpartlemd  31734  eulerpartlemgu  31745  eulerpartlemgf  31747  dstrvprob  31839  dstfrvel  31841  orvclteinc  31843  spthcycl  32489  cvmliftmolem1  32641  cvmliftlem3  32647  cvmliftlem10  32654  cvmliftlem13  32656  cvmlift2lem9  32671  cvmlift3lem6  32684  cvmlift3lem7  32685  satefvfmla0  32778  satefvfmla1  32785  msubrn  32889  mclsax  32929  mclsppslem  32943  mclspps  32944  ftc1cnnc  35129  heibor1lem  35247  grpokerinj  35331  lmhmfgima  40028  gneispacefun  40840  cncmpmax  41661  fidmfisupp  41828  limccog  42262  limsuppnfdlem  42343  climxrrelem  42391  climxrre  42392  liminfvalxr  42425  liminflimsupxrre  42459  xlimxrre  42473  dvsinax  42555  fvvolioof  42631  fvvolicof  42633  dirkercncflem2  42746  fourierdlem82  42830  subsaliuncllem  42997  fge0iccico  43009  sge0sn  43018  sge0tsms  43019  sge0cl  43020  sge0f1o  43021  sge0isum  43066  ovnovollem1  43295  ovnovollem2  43296  preimaioomnf  43354  smfresal  43420  smfres  43422  smfco  43434  isomushgr  44344  ushrisomgr  44359