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

Theorem ffun 5233
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 5230 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfun 5178 . 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 5075    Fn wfn 5076   -->wf 5077
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-fn 5084  df-f 5085
This theorem is referenced by:  ffund  5234  funssxp  5250  f00  5272  fofun  5304  fun11iun  5344  fimacnv  5503  dff3im  5519  resflem  5538  fmptco  5540  fliftf  5654  smores2  6145  pmfun  6516  elmapfun  6520  pmresg  6524  ac6sfi  6745  casef  6925  omp1eomlem  6931  ctm  6946  exmidfodomrlemim  7005  nn0supp  8933  frecuzrdg0  10079  frecuzrdgsuc  10080  frecuzrdgdomlem  10083  frecuzrdg0t  10088  frecuzrdgsuctlem  10089  climdm  10956  sum0  11049  isumz  11050  fsumsersdc  11056  isumclim  11082  iscnp3  12214  cnpnei  12230  cnclima  12234  cnrest2  12247  metcnp  12501  qtopbasss  12510  tgqioo  12533  dvaddxx  12622  dvmulxx  12623  dviaddf  12624  dvimulf  12625
  Copyright terms: Public domain W3C validator