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

Theorem f1fun 6553
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 6552 . 2 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
2 fnfun 6429 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 17 1 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Fun wfun 6325   Fn wfn 6326  1-1wf1 6328
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 209  df-an 399  df-fn 6334  df-f 6335  df-f1 6336
This theorem is referenced by:  f1cocnv2  6618  f1o2ndf1  7796  fnwelem  7803  f1dmvrnfibi  8786  fsuppco  8843  ackbij1b  9639  fin23lem31  9743  fin1a2lem6  9805  hashimarn  13786  gsumval3lem1  19004  gsumval3lem2  19005  usgrfun  26930  trlsegvdeglem6  27989  ccatf1  30612  cycpmrn  30793  cycpmconjslem2  30805  hashf1dmrn  32363  elhf  33643
  Copyright terms: Public domain W3C validator