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

Theorem ffun 5363
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 5360 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fnfun 5308 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 14 1 (𝐹:𝐴𝐵 → Fun 𝐹)
Colors of variables: wff set class
Syntax hints:  wi 4  Fun wfun 5205   Fn wfn 5206  wf 5207
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 5214  df-f 5215
This theorem is referenced by:  ffund  5364  funssxp  5380  f00  5402  fofun  5434  fun11iun  5477  fimacnv  5640  dff3im  5656  resflem  5675  fmptco  5677  fliftf  5793  smores2  6288  pmfun  6661  elmapfun  6665  pmresg  6669  ac6sfi  6891  casef  7080  omp1eomlem  7086  ctm  7101  exmidfodomrlemim  7193  nn0supp  9204  frecuzrdg0  10386  frecuzrdgsuc  10387  frecuzrdgdomlem  10390  frecuzrdg0t  10395  frecuzrdgsuctlem  10396  climdm  11274  sum0  11367  isumz  11368  fsumsersdc  11374  isumclim  11400  zprodap0  11560  iscnp3  13336  cnpnei  13352  cnclima  13356  cnrest2  13369  hmeores  13448  metcnp  13645  qtopbasss  13654  tgqioo  13680  dvaddxx  13800  dvmulxx  13801  dviaddf  13802  dvimulf  13803  dvef  13821  pilem3  13837
  Copyright terms: Public domain W3C validator