MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1ofun Structured 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 5697 . 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 5601    Fn wfn 5602   -1-1-onto->wf1o 5606
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 189  df-an 373  df-fn 5610  df-f 5611  df-f1 5612  df-f1o 5614
This theorem is referenced by:  f1orel  5840  f1oresrab  6076  fveqf1o  6221  isofrlem  6252  isofr  6254  isose  6255  f1opw  6543  xpcomco  7677  f1opwfi  7893  isercolllem2  13734  isercoll  13736  unbenlem  14857  gsumpropd2lem  16521  symgfixf1  17083  tgqtop  20731  hmeontr  20788  reghmph  20812  nrmhmph  20813  tgpconcompeqg  21130  cnheiborlem  21986  dfrelog  23519  dvloglem  23597  logf1o2  23599  axcontlem9  25006  axcontlem10  25007  eupares  25707  eupap1  25708  padct  28319  madjusmdetlem2  28668  tpr2rico  28732  ballotlemrv  29366  ballotlemrvOLD  29404  subfacp1lem2a  29917  subfacp1lem2b  29918  subfacp1lem5  29921  ismtyres  32110  diaclN  34593  dia1elN  34597  diaintclN  34601  docaclN  34667  dibintclN  34710  sge0f1o  38138
  Copyright terms: Public domain W3C validator