Theorem f1ofo 5468

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 5467	. 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 4625   Fun wfun 5210   -onto->wfo 5214   -1-1-onto->wf1o 5215

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223

This theorem is referenced by:  f1imacnv  5478  f1ococnv2  5488  fo00  5497  isoini  5818  isoselem  5820  f1opw2  6076  f1dmex  6116  bren  6746  f1oeng  6756  en1  6798  mapen  6845  ssenen  6850  phplem4  6854  phplem4on  6866  dif1en  6878  fiintim  6927  fidcenumlemim  6950  supisolem  7006  ordiso2  7033  djuunr  7064  omct  7115  ctssexmid  7147  1fv  10138  hashfacen  10815  fsumf1o  11397  fisumss  11399  fprodf1o  11595  fprodssdc  11597  ennnfonelemrn  12419  ennnfonelemnn0  12422  ennnfonelemim  12424  exmidunben  12426  ctinfomlemom  12427  ctinfom  12428  qnnen  12431  enctlem  12432  ssomct  12445  xpsfrn  12768  hmeontr  13783  hmeoimaf1o  13784  subctctexmid  14720  exmidsbthrlem  14740  sbthomlem  14743