Theorem f1ofo 5599

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 5598	. 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 4730   Fun wfun 5327   -onto->wfo 5331   -1-1-onto->wf1o 5332

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214  df-f 5337  df-f1 5338  df-fo 5339  df-f1o 5340

This theorem is referenced by:  f1imacnv  5609  f1ococnv2  5619  fo00  5630  isoini  5969  isoselem  5971  f1opw2  6239  f1dmex  6287  bren  6960  f1oeng  6973  en1  7016  mapen  7075  ssenen  7080  phplem4  7084  phplem4on  7097  dif1en  7111  fiintim  7166  fidcenumlemim  7194  supisolem  7267  ordiso2  7294  djuunr  7325  omct  7376  ctssexmid  7409  1fv  10436  hashfacen  11163  fsumf1o  12031  fisumss  12033  fprodf1o  12229  fprodssdc  12231  nninfct  12692  ennnfonelemrn  13120  ennnfonelemnn0  13123  ennnfonelemim  13125  exmidunben  13127  ctinfomlemom  13128  ctinfom  13129  qnnen  13132  enctlem  13133  ssomct  13146  xpsfrn  13513  imasmndf1  13617  imasgrpf1  13779  imasrngf1  14051  imasringf1  14159  znleval  14749  hmeontr  15124  hmeoimaf1o  15125  fsumdvdsmul  15805  eupthvdres  16416  subctctexmid  16722  domomsubct  16723  exmidsbthrlem  16750  sbthomlem  16753