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

Theorem f1ofun 5643
Description: A one-to-one onto mapping is a function. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1ofun  |-  ( F : A -1-1-onto-> B  ->  Fun  F )

Proof of Theorem f1ofun
StepHypRef Expression
1 f1ofn 5642 . 2  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
2 fnfun 5508 . 2  |-  ( F  Fn  A  ->  Fun  F )
31, 2syl 16 1  |-  ( F : A -1-1-onto-> B  ->  Fun  F )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   Fun wfun 5412    Fn wfn 5413   -1-1-onto->wf1o 5417
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 5421  df-f 5422  df-f1 5423  df-f1o 5425
This theorem is referenced by:  f1orel  5644  f1oresrab  5875  fveqf1o  6000  isofrlem  6031  isofr  6033  isose  6034  f1opw  6314  xpcomco  7401  f1opwfi  7615  mapfienOLD  7927  isercolllem2  13143  isercoll  13145  unbenlem  13969  gsumpropd2lem  15505  symgfixf1  15943  tgqtop  19285  hmeontr  19342  reghmph  19366  nrmhmph  19367  tgpconcompeqg  19682  cnheiborlem  20526  dfrelog  22017  dvloglem  22093  logf1o2  22095  axcontlem9  23218  axcontlem10  23219  eupares  23596  eupap1  23597  tpr2rico  26342  ballotlemrv  26902  subfacp1lem2a  27068  subfacp1lem2b  27069  subfacp1lem5  27072  ismtyres  28707  diaclN  34695  dia1elN  34699  diaintclN  34703  docaclN  34769  dibintclN  34812
  Copyright terms: Public domain W3C validator