Theorem f1ofo 5599

Description: A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004.)

Assertion

Ref	Expression
f1ofo	⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)

Proof of Theorem f1ofo

Step	Hyp	Ref	Expression
1		dff1o3 5598	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))
2	1	simplbi 274	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)

Syntax hints:   → wi 4  ^◡ccnv 4730  Fun wfun 5327  –onto→wfo 5331  –1-1-onto→wf1o 5332

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 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214  df-f 5337  df-f1 5338  df-fo 5339  df-f1o 5340

This theorem is referenced by:  f1imacnv  5609  f1ococnv2  5619  fo00  5630  isoini  5969  isoselem  5971  f1opw2  6239  f1dmex  6287  bren  6960  f1oeng  6973  en1  7016  mapen  7075  ssenen  7080  phplem4  7084  phplem4on  7097  dif1en  7111  fiintim  7166  fidcenumlemim  7194  supisolem  7250  ordiso2  7277  djuunr  7308  omct  7359  ctssexmid  7392  1fv  10419  hashfacen  11146  fsumf1o  12014  fisumss  12016  fprodf1o  12212  fprodssdc  12214  nninfct  12675  ennnfonelemrn  13103  ennnfonelemnn0  13106  ennnfonelemim  13108  exmidunben  13110  ctinfomlemom  13111  ctinfom  13112  qnnen  13115  enctlem  13116  ssomct  13129  xpsfrn  13496  imasmndf1  13600  imasgrpf1  13762  imasrngf1  14034  imasringf1  14142  znleval  14732  hmeontr  15107  hmeoimaf1o  15108  fsumdvdsmul  15788  eupthvdres  16399  subctctexmid  16705  domomsubct  16706  exmidsbthrlem  16733  sbthomlem  16736