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

Theorem ffund 6087
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 6086 . 2 (𝐹:𝐴𝐵 → Fun 𝐹)
31, 2syl 17 1 (𝜑 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 5920  wf 5922
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 5929  df-f 5930
This theorem is referenced by:  fofun  6154  fmptco  6436  evlslem3  19562  mdegldg  23871  uhgrfun  26006  vdegp1bi  26489  wlkreslem  26622  wlkres  26623  gneispacefun  38752  limsuppnfdlem  40251  climxrrelem  40299  climxrre  40300  liminfvalxr  40333  xlimxrre  40375  subsaliuncllem  40893  ovnovollem2  41192  preimaioomnf  41250  smfresal  41316  smfres  41318  smfco  41330
  Copyright terms: Public domain W3C validator