Theorem f1ofo 5623

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 5622	. 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 4750   Fun wfun 5348   -onto->wfo 5352   -1-1-onto->wf1o 5353

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 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3219  df-ss 3226  df-f 5358  df-f1 5359  df-fo 5360  df-f1o 5361

This theorem is referenced by:  f1imacnv  5633  f1ococnv2  5643  fo00  5654  isoini  5993  isoselem  5995  f1opw2  6263  f1dmex  6311  bren  6985  f1oeng  6998  en1  7041  mapen  7101  ssenen  7107  phplem4  7111  phplem4on  7124  dif1en  7138  fiintim  7193  fidcenumlemim  7224  supisolem  7301  ordiso2  7328  djuunr  7359  omct  7410  ctssexmid  7443  1fv  10477  hashfacen  11212  fsumf1o  12080  fisumss  12082  fprodf1o  12278  fprodssdc  12280  nninfct  12741  ennnfonelemrn  13187  ennnfonelemnn0  13190  ennnfonelemim  13192  exmidunben  13194  ctinfomlemom  13195  ctinfom  13196  qnnen  13199  enctlem  13200  ssomct  13213  xpsfrn  13580  imasmndf1  13684  imasgrpf1  13846  imasrngf1  14118  imasringf1  14226  znleval  14818  hmeontr  15195  hmeoimaf1o  15196  fsumdvdsmul  15876  eupthvdres  16487  subctctexmid  16791  domomsubct  16792  exmidsbthrlem  16819  sbthomlem  16822