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

Theorem ffun 5283
 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 5280 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fnfun 5228 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 14 1 (𝐹:𝐴𝐵 → Fun 𝐹)
 Colors of variables: wff set class Syntax hints:   → wi 4  Fun wfun 5125   Fn wfn 5126  ⟶wf 5127 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105 This theorem depends on definitions:  df-bi 116  df-fn 5134  df-f 5135 This theorem is referenced by:  ffund  5284  funssxp  5300  f00  5322  fofun  5354  fun11iun  5396  fimacnv  5557  dff3im  5573  resflem  5592  fmptco  5594  fliftf  5708  smores2  6199  pmfun  6570  elmapfun  6574  pmresg  6578  ac6sfi  6800  casef  6981  omp1eomlem  6987  ctm  7002  exmidfodomrlemim  7075  nn0supp  9054  frecuzrdg0  10218  frecuzrdgsuc  10219  frecuzrdgdomlem  10222  frecuzrdg0t  10227  frecuzrdgsuctlem  10228  climdm  11097  sum0  11190  isumz  11191  fsumsersdc  11197  isumclim  11223  zprodap0  11383  iscnp3  12412  cnpnei  12428  cnclima  12432  cnrest2  12445  hmeores  12524  metcnp  12721  qtopbasss  12730  tgqioo  12756  dvaddxx  12876  dvmulxx  12877  dviaddf  12878  dvimulf  12879  dvef  12897  pilem3  12913
 Copyright terms: Public domain W3C validator