Theorem f1ofo 5414

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 5413	. 2 |- ( F : A -1-1-onto-> B <-> ( F : A -onto-> B /\ Fun `' F ) )
2	1	simplbi 272	1 |- ( F : A -1-1-onto-> B -> F : A -onto-> B )

Syntax hints:   -> wi 4   `'ccnv 4578   Fun wfun 5157   -onto->wfo 5161   -1-1-onto->wf1o 5162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-11 1483  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-3an 965  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-in 3104  df-ss 3111  df-f 5167  df-f1 5168  df-fo 5169  df-f1o 5170

This theorem is referenced by:  f1imacnv  5424  f1ococnv2  5434  fo00  5443  isoini  5759  isoselem  5761  f1opw2  6016  f1dmex  6054  bren  6681  f1oeng  6691  en1  6733  mapen  6780  ssenen  6785  phplem4  6789  phplem4on  6801  dif1en  6813  fiintim  6862  fidcenumlemim  6885  supisolem  6940  ordiso2  6965  djuunr  6996  omct  7047  ctssexmid  7072  1fv  10016  hashfacen  10684  fsumf1o  11264  fisumss  11266  fprodf1o  11462  fprodssdc  11464  ennnfonelemrn  12099  ennnfonelemnn0  12102  ennnfonelemim  12104  exmidunben  12106  ctinfomlemom  12107  ctinfom  12108  qnnen  12111  enctlem  12112  hmeontr  12652  hmeoimaf1o  12653  subctctexmid  13512  exmidsbthrlem  13534  sbthomlem  13537