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

Theorem ffun 5387
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 5384 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfun 5332 . 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 5229    Fn wfn 5230   -->wf 5231
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 5238  df-f 5239
This theorem is referenced by:  ffund  5388  funssxp  5404  f00  5426  fofun  5458  fun11iun  5501  fimacnv  5666  dff3im  5682  resflem  5701  fmptco  5703  fliftf  5821  smores2  6319  pmfun  6694  elmapfun  6698  pmresg  6702  ac6sfi  6926  casef  7117  omp1eomlem  7123  ctm  7138  exmidfodomrlemim  7230  nn0supp  9258  frecuzrdg0  10444  frecuzrdgsuc  10445  frecuzrdgdomlem  10448  frecuzrdg0t  10453  frecuzrdgsuctlem  10454  climdm  11335  sum0  11428  isumz  11429  fsumsersdc  11435  isumclim  11461  zprodap0  11621  psrbaglesuppg  13950  iscnp3  14163  cnpnei  14179  cnclima  14183  cnrest2  14196  hmeores  14275  metcnp  14472  qtopbasss  14481  tgqioo  14507  dvaddxx  14627  dvmulxx  14628  dviaddf  14629  dvimulf  14630  dvef  14648  pilem3  14664
  Copyright terms: Public domain W3C validator