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

Theorem f1ofun 5818
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 5817 . 2  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
2 fnfun 5678 . 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 5582    Fn wfn 5583   -1-1-onto->wf1o 5587
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 5591  df-f 5592  df-f1 5593  df-f1o 5595
This theorem is referenced by:  f1orel  5819  f1oresrab  6053  fveqf1o  6193  isofrlem  6224  isofr  6226  isose  6227  f1opw  6513  xpcomco  7607  f1opwfi  7824  mapfienOLD  8138  isercolllem2  13451  isercoll  13453  unbenlem  14285  gsumpropd2lem  15827  symgfixf1  16268  tgqtop  19976  hmeontr  20033  reghmph  20057  nrmhmph  20058  tgpconcompeqg  20373  cnheiborlem  21217  dfrelog  22709  dvloglem  22785  logf1o2  22787  axcontlem9  23979  axcontlem10  23980  eupares  24679  eupap1  24680  tpr2rico  27558  ballotlemrv  28126  subfacp1lem2a  28292  subfacp1lem2b  28293  subfacp1lem5  28296  ismtyres  29935  diaclN  35865  dia1elN  35869  diaintclN  35873  docaclN  35939  dibintclN  35982
  Copyright terms: Public domain W3C validator