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

Theorem f1ofun 5474
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 5473 . 2  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
2 fnfun 5341 . 2  |-  ( F  Fn  A  ->  Fun  F )
31, 2syl 15 1  |-  ( F : A -1-1-onto-> B  ->  Fun  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4   Fun wfun 5249    Fn wfn 5250   -1-1-onto->wf1o 5254
This theorem is referenced by:  f1orel  5475  fveqf1o  5806  isofrlem  5837  isofr  5839  isose  5840  f1opw  6072  xpcomco  6952  f1opwfi  7159  mapfien  7399  isercolllem2  12139  isercoll  12141  unbenlem  12955  tgqtop  17403  hmeontr  17460  reghmph  17484  nrmhmph  17485  tgpconcompeqg  17794  cnheiborlem  18452  dfrelog  19923  dvloglem  19995  logf1o2  19997  ballotlemrv  23078  tpr2rico  23296  gsumpropd2lem  23379  subfacp1lem2a  23711  subfacp1lem2b  23712  subfacp1lem5  23715  eupares  23899  eupap1  23900  axcontlem9  24600  axcontlem10  24601  domrancur1c  25202  ismtyres  26532  diaclN  31240  dia1elN  31244  diaintclN  31248  docaclN  31314  dibintclN  31357
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-fn 5258  df-f 5259  df-f1 5260  df-f1o 5262
  Copyright terms: Public domain W3C validator