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

Theorem f1ofun 5635
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 5634 . 2  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
2 fnfun 5501 . 2  |-  ( F  Fn  A  ->  Fun  F )
31, 2syl 16 1  |-  ( F : A -1-1-onto-> B  ->  Fun  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4   Fun wfun 5407    Fn wfn 5408   -1-1-onto->wf1o 5412
This theorem is referenced by:  f1orel  5636  fveqf1o  5988  isofrlem  6019  isofr  6021  isose  6022  f1opw  6258  xpcomco  7157  f1opwfi  7368  mapfien  7609  isercolllem2  12414  isercoll  12416  unbenlem  13231  tgqtop  17697  hmeontr  17754  reghmph  17778  nrmhmph  17779  tgpconcompeqg  18094  cnheiborlem  18932  dfrelog  20416  dvloglem  20492  logf1o2  20494  eupares  21650  eupap1  21651  gsumpropd2lem  24173  tpr2rico  24263  ballotlemrv  24730  subfacp1lem2a  24819  subfacp1lem2b  24820  subfacp1lem5  24823  axcontlem9  25815  axcontlem10  25816  ismtyres  26407  diaclN  31533  dia1elN  31537  diaintclN  31541  docaclN  31607  dibintclN  31650
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 178  df-an 361  df-fn 5416  df-f 5417  df-f1 5418  df-f1o 5420
  Copyright terms: Public domain W3C validator