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

Theorem f1fun 5788
Description: A one-to-one mapping is a function. (Contributed by NM, 8-Mar-2014.)
Assertion
Ref Expression
f1fun

Proof of Theorem f1fun
StepHypRef Expression
1 f1fn 5787 . 2
2 fnfun 5683 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  Funwfun 5587  Fnwfn 5588  -1-1->wf1 5590
This theorem is referenced by:  f1cocnv2  5848  f1o2ndf1  6908  fnwelem  6915  fsuppco  7881  ackbij1b  8640  fin23lem31  8744  fin1a2lem6  8806  hashimarn  12496  gsumval3lem1  16909  gsumval3lem2  16910  usgrafun  24349  elhf  29831  f1dmvrnfibi  32312
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 185  df-an 371  df-fn 5596  df-f 5597  df-f1 5598
  Copyright terms: Public domain W3C validator