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

Theorem fnfun 5293
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 5199 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
21simplbi 272 1  |-  ( F  Fn  A  ->  Fun  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1348   dom cdm 4609   Fun wfun 5190    Fn wfn 5191
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-fn 5199
This theorem is referenced by:  fnrel  5294  funfni  5296  fnco  5304  fnssresb  5308  ffun  5348  f1fun  5404  f1ofun  5442  fnbrfvb  5535  fvelimab  5550  fvun1  5560  elpreima  5613  respreima  5622  fconst3m  5713  fnfvima  5728  fnunirn  5744  f1eqcocnv  5768  fnexALT  6088  tfrlem4  6290  tfrlem5  6291  fndmeng  6786  caseinl  7066  caseinr  7067  cc2lem  7221  shftfn  10781  phimullem  12172  qnnen  12379
  Copyright terms: Public domain W3C validator