Theorem f1ofo 5621

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 5620	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))
2	1	simplbi 274	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)

Syntax hints:   → wi 4  ^◡ccnv 4748  Fun wfun 5346  –onto→wfo 5350  –1-1-onto→wf1o 5351

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 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224  df-f 5356  df-f1 5357  df-fo 5358  df-f1o 5359

This theorem is referenced by:  f1imacnv  5631  f1ococnv2  5641  fo00  5652  isoini  5991  isoselem  5993  f1opw2  6261  f1dmex  6309  bren  6983  f1oeng  6996  en1  7039  mapen  7099  ssenen  7105  phplem4  7109  phplem4on  7122  dif1en  7136  fiintim  7191  fidcenumlemim  7222  supisolem  7299  ordiso2  7326  djuunr  7357  omct  7408  ctssexmid  7441  1fv  10473  hashfacen  11208  fsumf1o  12076  fisumss  12078  fprodf1o  12274  fprodssdc  12276  nninfct  12737  ennnfonelemrn  13170  ennnfonelemnn0  13173  ennnfonelemim  13175  exmidunben  13177  ctinfomlemom  13178  ctinfom  13179  qnnen  13182  enctlem  13183  ssomct  13196  xpsfrn  13563  imasmndf1  13667  imasgrpf1  13829  imasrngf1  14101  imasringf1  14209  znleval  14801  hmeontr  15178  hmeoimaf1o  15179  fsumdvdsmul  15859  eupthvdres  16470  subctctexmid  16774  domomsubct  16775  exmidsbthrlem  16802  sbthomlem  16805