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

Theorem f1ofun 5833
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 5832 . 2  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
2 fnfun 5691 . 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 5595    Fn wfn 5596   -1-1-onto->wf1o 5600
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 188  df-an 372  df-fn 5604  df-f 5605  df-f1 5606  df-f1o 5608
This theorem is referenced by:  f1orel  5834  f1oresrab  6070  fveqf1o  6215  isofrlem  6246  isofr  6248  isose  6249  f1opw  6537  xpcomco  7668  f1opwfi  7884  isercolllem2  13707  isercoll  13709  unbenlem  14815  gsumpropd2lem  16467  symgfixf1  17029  tgqtop  20658  hmeontr  20715  reghmph  20739  nrmhmph  20740  tgpconcompeqg  21057  cnheiborlem  21878  dfrelog  23380  dvloglem  23458  logf1o2  23460  axcontlem9  24848  axcontlem10  24849  eupares  25548  eupap1  25549  padct  28150  madjusmdetlem2  28493  tpr2rico  28557  ballotlemrv  29178  subfacp1lem2a  29691  subfacp1lem2b  29692  subfacp1lem5  29695  ismtyres  31844  diaclN  34327  dia1elN  34331  diaintclN  34335  docaclN  34401  dibintclN  34444  sge0f1o  37758
  Copyright terms: Public domain W3C validator