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

Theorem fnfund 6655
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 6654 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝜑 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6542   Fn wfn 6543
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 206  df-an 396  df-fn 6551
This theorem is referenced by:  imadrhmcl  20685  noseqrdg0  28193  noseqrdgsuc  28194  ply1degltdimlem  33320  bnj945  34404  bnj545  34526  bnj548  34528  bnj553  34529  bnj570  34536  bnj929  34567  bnj966  34575  bnj1442  34680  bnj1450  34681  bnj1501  34698  aks6d1c2lem4  41598  aks6d1c2  41601  aks6d1c6lem5  41649  eqresfnbd  41723
  Copyright terms: Public domain W3C validator