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

Theorem ffund 6162
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 6161 . 2 (𝐹:𝐴𝐵 → Fun 𝐹)
31, 2syl 17 1 (𝜑 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 5995  wf 5997
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 197  df-an 385  df-fn 6004  df-f 6005
This theorem is referenced by:  fofun  6229  fmptco  6511  evlslem3  19637  mdegldg  23946  uhgrfun  26081  vdegp1bi  26564  wlkreslem  26697  wlkres  26698  gneispacefun  38854  limsuppnfdlem  40353  climxrrelem  40401  climxrre  40402  liminfvalxr  40435  xlimxrre  40477  subsaliuncllem  40995  ovnovollem2  41294  preimaioomnf  41352  smfresal  41418  smfres  41420  smfco  41432
  Copyright terms: Public domain W3C validator