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

Theorem f1fun 6741
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 6740 . 2 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
2 fnfun 6603 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6491   Fn wfn 6492  1-1wf1 6494
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 206  df-an 398  df-fn 6500  df-f 6501  df-f1 6502
This theorem is referenced by:  f1cocnv2  6813  f1o2ndf1  8055  fnwelem  8064  f1dmvrnfibi  9281  fsuppco  9339  ackbij1b  10176  fin23lem31  10280  fin1a2lem6  10342  hashimarn  14341  gsumval3lem1  19683  gsumval3lem2  19684  usgrfun  28112  trlsegvdeglem6  29172  ccatf1  31808  cycpmrn  31995  cycpmconjslem2  32007  hashf1dmrn  33710  elhf  34762
  Copyright terms: Public domain W3C validator