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

Theorem f1ofun 5839
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 5838 . 2  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
2 fnfun 5695 . 2  |-  ( F  Fn  A  ->  Fun  F )
31, 2syl 17 1  |-  ( F : A -1-1-onto-> B  ->  Fun  F )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   Fun wfun 5595    Fn wfn 5596   -1-1-onto->wf1o 5600
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 190  df-an 377  df-fn 5604  df-f 5605  df-f1 5606  df-f1o 5608
This theorem is referenced by:  f1orel  5840  f1oresrab  6079  fveqf1o  6225  isofrlem  6256  isofr  6258  isose  6259  f1opw  6550  xpcomco  7688  f1opwfi  7904  isercolllem2  13778  isercoll  13780  unbenlem  14901  gsumpropd2lem  16565  symgfixf1  17127  tgqtop  20776  hmeontr  20833  reghmph  20857  nrmhmph  20858  tgpconcompeqg  21175  cnheiborlem  22031  dfrelog  23564  dvloglem  23642  logf1o2  23644  axcontlem9  25051  axcontlem10  25052  eupares  25752  eupap1  25753  padct  28356  madjusmdetlem2  28703  tpr2rico  28767  ballotlemrv  29401  ballotlemrvOLD  29439  subfacp1lem2a  29952  subfacp1lem2b  29953  subfacp1lem5  29956  ismtyres  32185  diaclN  34663  dia1elN  34667  diaintclN  34671  docaclN  34737  dibintclN  34780  sge0f1o  38262
  Copyright terms: Public domain W3C validator