Theorem f1ofo 5374

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 5373	. 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 4538   Fun wfun 5117   -onto->wfo 5121   -1-1-onto->wf1o 5122

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130

This theorem is referenced by:  f1imacnv  5384  f1ococnv2  5394  fo00  5403  isoini  5719  isoselem  5721  f1opw2  5976  f1dmex  6014  bren  6641  f1oeng  6651  en1  6693  mapen  6740  ssenen  6745  phplem4  6749  phplem4on  6761  dif1en  6773  fiintim  6817  fidcenumlemim  6840  supisolem  6895  ordiso2  6920  djuunr  6951  omct  7002  ctssexmid  7024  1fv  9916  hashfacen  10579  fsumf1o  11159  fisumss  11161  ennnfonelemrn  11932  ennnfonelemnn0  11935  ennnfonelemim  11937  exmidunben  11939  ctinfomlemom  11940  ctinfom  11941  qnnen  11944  enctlem  11945  hmeontr  12482  hmeoimaf1o  12483  subctctexmid  13196  exmidsbthrlem  13217  sbthomlem  13220