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

Theorem fnfund 6670
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 6669 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝜑 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6557   Fn wfn 6558
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 6566
This theorem is referenced by:  imadrhmcl  20815  noseqrdg0  28328  noseqrdgsuc  28329  ply1degltdimlem  33650  bnj945  34766  bnj545  34888  bnj548  34890  bnj553  34891  bnj570  34898  bnj929  34929  bnj966  34937  bnj1442  35042  bnj1450  35043  bnj1501  35060  aks6d1c2lem4  42109  aks6d1c2  42112  aks6d1c6lem5  42159  eqresfnbd  42252
  Copyright terms: Public domain W3C validator