MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1fun Structured version   Visualization version   GIF version

Theorem f1fun 6000
Description: A one-to-one mapping is a function. (Contributed by NM, 8-Mar-2014.)
Assertion
Ref Expression
f1fun (𝐹:𝐴1-1𝐵 → Fun 𝐹)

Proof of Theorem f1fun
StepHypRef Expression
1 f1fn 5999 . 2 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
2 fnfun 5887 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 5783   Fn wfn 5784  1-1wf1 5786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 195  df-an 384  df-fn 5792  df-f 5793  df-f1 5794
This theorem is referenced by:  f1cocnv2  6061  f1o2ndf1  7149  fnwelem  7156  f1dmvrnfibi  8110  fsuppco  8167  ackbij1b  8921  fin23lem31  9025  fin1a2lem6  9087  hashimarn  13039  gsumval3lem1  18077  gsumval3lem2  18078  usgrafun  25671  elhf  31244  usgrfun  40369  trlsegvdeglem6  41374
  Copyright terms: Public domain W3C validator