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

Theorem f1fun 6570
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 6569 . 2 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
2 fnfun 6446 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6342   Fn wfn 6343  1-1wf1 6345
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 208  df-an 397  df-fn 6351  df-f 6352  df-f1 6353
This theorem is referenced by:  f1cocnv2  6635  f1o2ndf1  7807  fnwelem  7814  f1dmvrnfibi  8796  fsuppco  8853  ackbij1b  9649  fin23lem31  9753  fin1a2lem6  9815  hashimarn  13789  gsumval3lem1  18954  gsumval3lem2  18955  usgrfun  26870  trlsegvdeglem6  27931  ccatf1  30552  cycpmrn  30712  cycpmconjslem2  30724  hashf1dmrn  32252  elhf  33532
  Copyright terms: Public domain W3C validator