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

Theorem fnfun 5335
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 5241 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
21simplbi 274 1  |-  ( F  Fn  A  ->  Fun  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1364   dom cdm 4647   Fun wfun 5232    Fn wfn 5233
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem depends on definitions:  df-bi 117  df-fn 5241
This theorem is referenced by:  fnrel  5336  funfni  5338  fnco  5346  fnssresb  5350  ffun  5390  f1fun  5446  f1ofun  5485  fnbrfvb  5580  fvelimab  5596  fvun1  5606  elpreima  5659  respreima  5668  fconst3m  5759  fnfvima  5775  fnunirn  5792  f1eqcocnv  5816  fnexALT  6140  tfrlem4  6342  tfrlem5  6343  fndmeng  6840  caseinl  7124  caseinr  7125  cc2lem  7300  shftfn  10874  phimullem  12268  qnnen  12493  prdsex  12785  imasaddvallemg  12803  lidlmex  13816
  Copyright terms: Public domain W3C validator