Theorem f1ofo 5260

Description: A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004.)

Assertion

Ref	Expression
f1ofo	|- ( F : A -1-1-onto-> B -> F : A -onto-> B )

Proof of Theorem f1ofo

Step	Hyp	Ref	Expression
1		dff1o3 5259	. 2 |- ( F : A -1-1-onto-> B <-> ( F : A -onto-> B /\ Fun `' F ) )
2	1	simplbi 268	1 |- ( F : A -1-1-onto-> B -> F : A -onto-> B )

Syntax hints:   -> wi 4   `'ccnv 4437   Fun wfun 5009   -onto->wfo 5013   -1-1-onto->wf1o 5014

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-3an 926  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-in 3005  df-ss 3012  df-f 5019  df-f1 5020  df-fo 5021  df-f1o 5022

This theorem is referenced by:  f1imacnv  5270  f1ococnv2  5280  fo00  5289  isoini  5597  isoselem  5599  f1opw2  5850  f1dmex  5887  bren  6464  f1oeng  6474  en1  6516  mapen  6562  ssenen  6567  phplem4  6571  phplem4on  6583  dif1en  6595  fiintim  6639  fidcenumlemim  6661  supisolem  6703  ordiso2  6728  djuunr  6758  1fv  9550  hashfacen  10241  fsumf1o  10782  fisumss  10784  exmidsbthrlem  11912