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

Theorem ffun 5073
Description: A mapping is a function. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
ffun (𝐹:𝐴𝐵 → Fun 𝐹)

Proof of Theorem ffun
StepHypRef Expression
1 ffn 5071 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fnfun 5021 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 14 1 (𝐹:𝐴𝐵 → Fun 𝐹)
Colors of variables: wff set class
Syntax hints:  wi 4  Fun wfun 4920   Fn wfn 4921  wf 4922
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 4929  df-f 4930
This theorem is referenced by:  funssxp  5085  f00  5106  fofun  5132  fun11iun  5172  fimacnv  5322  dff3im  5338  fmptco  5356  fliftf  5464  smores2  5937  ac6sfi  6421  nn0supp  8396  frecuzrdg0  9484  frecuzrdgsuc  9485  frecuzrdgdomlem  9488  frecuzrdg0t  9493  frecuzrdgsuctlem  9494  climdm  10261
  Copyright terms: Public domain W3C validator