Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ffund Structured version   Visualization version   GIF version

Theorem ffund 6517
 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
StepHypRef Expression
1 ffund.1 . 2 (𝜑𝐹:𝐴𝐵)
2 ffun 6516 . 2 (𝐹:𝐴𝐵 → Fun 𝐹)
31, 2syl 17 1 (𝜑 → Fun 𝐹)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  Fun wfun 6348  ⟶wf 6350 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 208  df-an 397  df-fn 6357  df-f 6358 This theorem is referenced by:  fofun  6590  fmptco  6889  smores2  7987  elmapfun  8425  fdmfifsupp  8837  fsuppmptif  8857  fsuppco2  8860  fsuppcor  8861  ordtypelem8  8983  ordtypelem9  8984  ordtypelem10  8985  unxpwdom2  9046  fpwwe2  10059  swrdwrdsymb  14019  mrcuni  16887  frmdss2  18023  cntzmhm2  18415  frgpupval  18836  gsumzadd  18978  gsumpt  19018  gsum2dlem2  19027  dprd2da  19100  lmhmpreima  19756  lmhmlsp  19757  psrelbasfun  20095  mvrcl  20164  evlslem3  20228  evlseu  20231  mpfind  20255  gsumply1subr  20337  cygznlem2  20650  frlmsslsp  20875  frlmup1  20877  frlmup4  20880  lindff1  20899  lindfrn  20900  cnclsi  21815  cncnp  21823  paste  21837  connima  21968  1stcfb  21988  1stccnp  22005  1stckgenlem  22096  txcnpi  22151  txcnp  22163  xkoco2cn  22201  fmfnfmlem2  22498  lmflf  22548  txflf  22549  cnextcn  22610  clssubg  22651  ghmcnp  22657  metustid  23098  metustexhalf  23100  isngp2  23140  pi1xfrval  23592  pi1coval  23598  iscfil2  23803  rrxcph  23929  ismbfd  24174  ellimc2  24409  ellimc3  24411  dvres3  24445  dvres3a  24446  dvcnv  24508  dvcnvrelem1  24548  ftc1cn  24574  mdegldg  24594  plyeq0  24735  plyaddlem1  24737  plymullem1  24738  ulmdv  24925  dchrelbas2  25746  dchrghm  25765  uhgrfun  26784  vdegp1ai  27251  vdegp1bi  27252  wlkres  27385  sspg  28438  ssps  28440  sspn  28446  htthlem  28627  fmptcof2  30336  fnpreimac  30350  curry2ima  30376  offinsupp1  30395  fpwrelmapffslem  30400  swrdrn2  30561  xrge0tsmsd  30625  cyc3co2  30715  tocyccntz  30719  rmfsupp2  30799  lbsdiflsp0  30927  fedgmullem1  30930  fedgmullem2  30931  esumpfinvallem  31238  sibfof  31503  sitgclg  31505  eulerpartlemd  31529  eulerpartlemgu  31540  eulerpartlemgf  31542  dstrvprob  31634  dstfrvel  31636  orvclteinc  31638  spthcycl  32279  cvmliftmolem1  32431  cvmliftlem3  32437  cvmliftlem10  32444  cvmliftlem13  32446  cvmlift2lem9  32461  cvmlift3lem6  32474  cvmlift3lem7  32475  satefvfmla0  32568  satefvfmla1  32575  msubrn  32679  mclsax  32719  mclsppslem  32733  mclspps  32734  ftc1cnnc  34852  heibor1lem  34974  grpokerinj  35058  lmhmfgima  39568  gneispacefun  40371  funfvima2d  40404  cncmpmax  41173  fidmfisupp  41346  limccog  41785  limsuppnfdlem  41866  climxrrelem  41914  climxrre  41915  liminfvalxr  41948  liminflimsupxrre  41982  xlimxrre  41996  dvsinax  42081  fvvolioof  42159  fvvolicof  42161  dirkercncflem2  42274  fourierdlem82  42358  subsaliuncllem  42525  fge0iccico  42537  sge0sn  42546  sge0tsms  42547  sge0cl  42548  sge0f1o  42549  sge0isum  42594  ovnovollem1  42823  ovnovollem2  42824  preimaioomnf  42882  smfresal  42948  smfres  42950  smfco  42962  isomushgr  43842  ushrisomgr  43857
 Copyright terms: Public domain W3C validator