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

Theorem fnfund 6680
Description: A function with domain is a function, deduction form. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
fnfund.1 (𝜑𝐹 Fn 𝐴)
Assertion
Ref Expression
fnfund (𝜑 → Fun 𝐹)

Proof of Theorem fnfund
StepHypRef Expression
1 fnfund.1 . 2 (𝜑𝐹 Fn 𝐴)
2 fnfun 6679 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝜑 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6567   Fn wfn 6568
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 207  df-an 396  df-fn 6576
This theorem is referenced by:  imadrhmcl  20820  noseqrdg0  28331  noseqrdgsuc  28332  ply1degltdimlem  33635  bnj945  34749  bnj545  34871  bnj548  34873  bnj553  34874  bnj570  34881  bnj929  34912  bnj966  34920  bnj1442  35025  bnj1450  35026  bnj1501  35043  aks6d1c2lem4  42084  aks6d1c2  42087  aks6d1c6lem5  42134  eqresfnbd  42227
  Copyright terms: Public domain W3C validator