Theorem f1ofo 5579

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

Syntax hints:   -> wi 4   `'ccnv 4718   Fun wfun 5312   -onto->wfo 5316   -1-1-onto->wf1o 5317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210  df-f 5322  df-f1 5323  df-fo 5324  df-f1o 5325

This theorem is referenced by:  f1imacnv  5589  f1ococnv2  5599  fo00  5609  isoini  5942  isoselem  5944  f1opw2  6212  f1dmex  6261  bren  6895  f1oeng  6908  en1  6951  mapen  7007  ssenen  7012  phplem4  7016  phplem4on  7029  dif1en  7041  fiintim  7093  fidcenumlemim  7119  supisolem  7175  ordiso2  7202  djuunr  7233  omct  7284  ctssexmid  7317  1fv  10335  hashfacen  11058  fsumf1o  11901  fisumss  11903  fprodf1o  12099  fprodssdc  12101  nninfct  12562  ennnfonelemrn  12990  ennnfonelemnn0  12993  ennnfonelemim  12995  exmidunben  12997  ctinfomlemom  12998  ctinfom  12999  qnnen  13002  enctlem  13003  ssomct  13016  xpsfrn  13383  imasmndf1  13487  imasgrpf1  13649  imasrngf1  13920  imasringf1  14028  znleval  14617  hmeontr  14987  hmeoimaf1o  14988  fsumdvdsmul  15665  subctctexmid  16366  domomsubct  16367  exmidsbthrlem  16390  sbthomlem  16393