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

Theorem ffun 5164
Description: A mapping is a function. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
ffun  |-  ( F : A --> B  ->  Fun  F )

Proof of Theorem ffun
StepHypRef Expression
1 ffn 5161 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfun 5111 . 2  |-  ( F  Fn  A  ->  Fun  F )
31, 2syl 14 1  |-  ( F : A --> B  ->  Fun  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4   Fun wfun 5009    Fn wfn 5010   -->wf 5011
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  df-f 5019
This theorem is referenced by:  funssxp  5180  f00  5202  fofun  5234  fun11iun  5274  fimacnv  5428  dff3im  5444  resflem  5462  fmptco  5464  fliftf  5578  smores2  6059  pmfun  6423  elmapfun  6427  pmresg  6431  ac6sfi  6612  casef  6777  exmidfodomrlemim  6825  nn0supp  8723  frecuzrdg0  9816  frecuzrdgsuc  9817  frecuzrdgdomlem  9820  frecuzrdg0t  9825  frecuzrdgsuctlem  9826  climdm  10679  sum0  10776  isumz  10777  fisumsers  10784  isumclim  10811
  Copyright terms: Public domain W3C validator