Theorem f1ofo 5581

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 5580	. 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 4718   Fun wfun 5312   -onto->wfo 5316   -1-1-onto->wf1o 5317

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210  df-f 5322  df-f1 5323  df-fo 5324  df-f1o 5325

This theorem is referenced by:  f1imacnv  5591  f1ococnv2  5601  fo00  5611  isoini  5948  isoselem  5950  f1opw2  6218  f1dmex  6267  bren  6903  f1oeng  6916  en1  6959  mapen  7015  ssenen  7020  phplem4  7024  phplem4on  7037  dif1en  7049  fiintim  7104  fidcenumlemim  7130  supisolem  7186  ordiso2  7213  djuunr  7244  omct  7295  ctssexmid  7328  1fv  10347  hashfacen  11071  fsumf1o  11917  fisumss  11919  fprodf1o  12115  fprodssdc  12117  nninfct  12578  ennnfonelemrn  13006  ennnfonelemnn0  13009  ennnfonelemim  13011  exmidunben  13013  ctinfomlemom  13014  ctinfom  13015  qnnen  13018  enctlem  13019  ssomct  13032  xpsfrn  13399  imasmndf1  13503  imasgrpf1  13665  imasrngf1  13936  imasringf1  14044  znleval  14633  hmeontr  15003  hmeoimaf1o  15004  fsumdvdsmul  15681  subctctexmid  16453  domomsubct  16454  exmidsbthrlem  16478  sbthomlem  16481