Theorem f1ofo 5644

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 5643	. 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 4771   Fun wfun 5369   -onto->wfo 5373   -1-1-onto->wf1o 5374

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233  df-f 5379  df-f1 5380  df-fo 5381  df-f1o 5382

This theorem is referenced by:  f1imacnv  5654  f1ococnv2  5664  fo00  5675  isoini  6017  isoselem  6019  f1opw2  6289  f1dmex  6338  bren  7023  f1oeng  7036  en1  7079  mapen  7139  ssenen  7145  phplem4  7149  phplem4on  7162  dif1en  7176  fiintim  7231  fidcenumlemim  7262  supisolem  7341  ordiso2  7368  djuunr  7399  omct  7450  ctssexmid  7483  1fv  10527  hashfacen  11265  fsumf1o  12138  fisumss  12140  fprodf1o  12336  fprodssdc  12338  nninfct  12799  ballotfilemro  13247  ennnfonelemrn  13291  ennnfonelemnn0  13294  ennnfonelemim  13296  exmidunben  13298  ctinfomlemom  13299  ctinfom  13300  qnnen  13303  enctlem  13304  ssomct  13317  xpsfrn  13651  imasmndf1  13741  imasgrpf1  13895  imasrngf1  14234  imasringf1  14346  znleval  14963  hmeontr  15340  hmeoimaf1o  15341  fsumdvdsmul  16022  eupthvdres  16633  subctctexmid  16947  domomsubct  16948  exmidsbthrlem  16975  sbthomlem  16978