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

Theorem fnfund 6668
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 6667 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝜑 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6554   Fn wfn 6555
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 6563
This theorem is referenced by:  imadrhmcl  20799  noseqrdg0  28314  noseqrdgsuc  28315  ply1degltdimlem  33674  bnj945  34788  bnj545  34910  bnj548  34912  bnj553  34913  bnj570  34920  bnj929  34951  bnj966  34959  bnj1442  35064  bnj1450  35065  bnj1501  35082  aks6d1c2lem4  42129  aks6d1c2  42132  aks6d1c6lem5  42179  eqresfnbd  42273
  Copyright terms: Public domain W3C validator