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

Theorem f1fun 6789
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 6788 . 2 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
2 fnfun 6649 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6537   Fn wfn 6538  1-1wf1 6540
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 396  df-fn 6546  df-f 6547  df-f1 6548
This theorem is referenced by:  f1cocnv2  6861  f1o2ndf1  8113  fnwelem  8122  f1dmvrnfibi  9342  fsuppco  9403  ackbij1b  10240  fin23lem31  10344  fin1a2lem6  10406  hashimarn  14407  hashf1dmrn  14410  gsumval3lem1  19821  gsumval3lem2  19822  usgrfun  28851  trlsegvdeglem6  29911  ccatf1  32548  cycpmrn  32738  cycpmconjslem2  32750  elhf  35616
  Copyright terms: Public domain W3C validator