ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fnfun Unicode version

Theorem fnfun 5111
Description: A function with domain is a function. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
fnfun  |-  ( F  Fn  A  ->  Fun  F )

Proof of Theorem fnfun
StepHypRef Expression
1 df-fn 5018 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
21simplbi 268 1  |-  ( F  Fn  A  ->  Fun  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1289   dom cdm 4438   Fun wfun 5009    Fn wfn 5010
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-fn 5018
This theorem is referenced by:  fnrel  5112  funfni  5114  fnco  5122  fnssresb  5126  ffun  5164  f1fun  5219  f1ofun  5255  fnbrfvb  5345  fvelimab  5360  fvun1  5370  elpreima  5418  respreima  5427  fconst3m  5516  fnfvima  5529  fnunirn  5546  f1eqcocnv  5570  fnexALT  5884  tfrlem4  6078  tfrlem5  6079  fndmeng  6525  shftfn  10254  phimullem  11475
  Copyright terms: Public domain W3C validator