Theorem f1ofo 5512

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 5511	. 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  5522  f1ococnv2  5532  fo00  5541  isoini  5866  isoselem  5868  f1opw2  6130  f1dmex  6174  bren  6807  f1oeng  6817  en1  6859  mapen  6908  ssenen  6913  phplem4  6917  phplem4on  6929  dif1en  6941  fiintim  6993  fidcenumlemim  7019  supisolem  7075  ordiso2  7102  djuunr  7133  omct  7184  ctssexmid  7217  1fv  10216  hashfacen  10930  fsumf1o  11557  fisumss  11559  fprodf1o  11755  fprodssdc  11757  nninfct  12218  ennnfonelemrn  12646  ennnfonelemnn0  12649  ennnfonelemim  12651  exmidunben  12653  ctinfomlemom  12654  ctinfom  12655  qnnen  12658  enctlem  12659  ssomct  12672  xpsfrn  13003  imasgrpf1  13252  imasrngf1  13523  imasringf1  13631  znleval  14219  hmeontr  14559  hmeoimaf1o  14560  fsumdvdsmul  15237  subctctexmid  15655  exmidsbthrlem  15676  sbthomlem  15679