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

Theorem fnfun 5027
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 4935 . 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 1285   dom cdm 4371   Fun wfun 4926    Fn wfn 4927
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 4935
This theorem is referenced by:  fnrel  5028  funfni  5030  fnco  5038  fnssresb  5042  ffun  5079  f1fun  5125  f1ofun  5159  fnbrfvb  5246  fvelimab  5261  fvun1  5271  elpreima  5318  respreima  5327  fconst3m  5412  fnfvima  5425  fnunirn  5438  f1eqcocnv  5462  fnexALT  5771  tfrlem4  5962  tfrlem5  5963  fndmeng  6357  shftfn  9850
  Copyright terms: Public domain W3C validator