Theorem f1ofo 5641

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

Syntax hints:   → wi 4  ^◡ccnv 4768  Fun wfun 5366  –onto→wfo 5370  –1-1-onto→wf1o 5371

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233  df-f 5376  df-f1 5377  df-fo 5378  df-f1o 5379

This theorem is referenced by:  f1imacnv  5651  f1ococnv2  5661  fo00  5672  isoini  6014  isoselem  6016  f1opw2  6286  f1dmex  6335  bren  7020  f1oeng  7033  en1  7076  mapen  7136  ssenen  7142  phplem4  7146  phplem4on  7159  dif1en  7173  fiintim  7228  fidcenumlemim  7259  supisolem  7338  ordiso2  7365  djuunr  7396  omct  7447  ctssexmid  7480  1fv  10524  hashfacen  11262  fsumf1o  12135  fisumss  12137  fprodf1o  12333  fprodssdc  12335  nninfct  12796  ballotfilemro  13244  ennnfonelemrn  13288  ennnfonelemnn0  13291  ennnfonelemim  13293  exmidunben  13295  ctinfomlemom  13296  ctinfom  13297  qnnen  13300  enctlem  13301  ssomct  13314  xpsfrn  13648  imasmndf1  13738  imasgrpf1  13892  imasrngf1  14231  imasringf1  14343  znleval  14960  hmeontr  15337  hmeoimaf1o  15338  fsumdvdsmul  16019  eupthvdres  16630  subctctexmid  16944  domomsubct  16945  exmidsbthrlem  16972  sbthomlem  16975