Theorem f1ofo 5514

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 5513	. 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 4663   Fun wfun 5253   -onto->wfo 5257   -1-1-onto->wf1o 5258

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170  df-f 5263  df-f1 5264  df-fo 5265  df-f1o 5266

This theorem is referenced by:  f1imacnv  5524  f1ococnv2  5534  fo00  5543  isoini  5868  isoselem  5870  f1opw2  6133  f1dmex  6182  bren  6815  f1oeng  6825  en1  6867  mapen  6916  ssenen  6921  phplem4  6925  phplem4on  6937  dif1en  6949  fiintim  7001  fidcenumlemim  7027  supisolem  7083  ordiso2  7110  djuunr  7141  omct  7192  ctssexmid  7225  1fv  10231  hashfacen  10945  fsumf1o  11572  fisumss  11574  fprodf1o  11770  fprodssdc  11772  nninfct  12233  ennnfonelemrn  12661  ennnfonelemnn0  12664  ennnfonelemim  12666  exmidunben  12668  ctinfomlemom  12669  ctinfom  12670  qnnen  12673  enctlem  12674  ssomct  12687  xpsfrn  13052  imasmndf1  13156  imasgrpf1  13318  imasrngf1  13589  imasringf1  13697  znleval  14285  hmeontr  14633  hmeoimaf1o  14634  fsumdvdsmul  15311  subctctexmid  15731  domomsubct  15732  exmidsbthrlem  15753  sbthomlem  15756