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

Theorem f1ofun 5640
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 5639 . 2  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
2 fnfun 5505 . 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 5409    Fn wfn 5410   -1-1-onto->wf1o 5414
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 5418  df-f 5419  df-f1 5420  df-f1o 5422
This theorem is referenced by:  f1orel  5641  f1oresrab  5872  fveqf1o  5997  isofrlem  6028  isofr  6030  isose  6031  f1opw  6313  xpcomco  7397  f1opwfi  7611  mapfienOLD  7923  isercolllem2  13139  isercoll  13141  unbenlem  13965  symgfixf1  15936  tgqtop  19185  hmeontr  19242  reghmph  19266  nrmhmph  19267  tgpconcompeqg  19582  cnheiborlem  20426  dfrelog  21960  dvloglem  22036  logf1o2  22038  axcontlem9  23137  axcontlem10  23138  eupares  23515  eupap1  23516  gsumpropd2lem  26161  tpr2rico  26262  ballotlemrv  26816  subfacp1lem2a  26982  subfacp1lem2b  26983  subfacp1lem5  26986  ismtyres  28616  diaclN  34383  dia1elN  34387  diaintclN  34391  docaclN  34457  dibintclN  34500
  Copyright terms: Public domain W3C validator