Theorem f1ofo 5531

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 5530	. 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 4675   Fun wfun 5266   -onto->wfo 5270   -1-1-onto->wf1o 5271

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179  df-f 5276  df-f1 5277  df-fo 5278  df-f1o 5279

This theorem is referenced by:  f1imacnv  5541  f1ococnv2  5551  fo00  5560  isoini  5889  isoselem  5891  f1opw2  6154  f1dmex  6203  bren  6837  f1oeng  6850  en1  6893  mapen  6945  ssenen  6950  phplem4  6954  phplem4on  6966  dif1en  6978  fiintim  7030  fidcenumlemim  7056  supisolem  7112  ordiso2  7139  djuunr  7170  omct  7221  ctssexmid  7254  1fv  10263  hashfacen  10983  fsumf1o  11734  fisumss  11736  fprodf1o  11932  fprodssdc  11934  nninfct  12395  ennnfonelemrn  12823  ennnfonelemnn0  12826  ennnfonelemim  12828  exmidunben  12830  ctinfomlemom  12831  ctinfom  12832  qnnen  12835  enctlem  12836  ssomct  12849  xpsfrn  13215  imasmndf1  13319  imasgrpf1  13481  imasrngf1  13752  imasringf1  13860  znleval  14448  hmeontr  14818  hmeoimaf1o  14819  fsumdvdsmul  15496  subctctexmid  15974  domomsubct  15975  exmidsbthrlem  15998  sbthomlem  16001