Theorem f1ofo 5587

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

Syntax hints:   → wi 4  ^◡ccnv 4722  Fun wfun 5318  –onto→wfo 5322  –1-1-onto→wf1o 5323

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211  df-f 5328  df-f1 5329  df-fo 5330  df-f1o 5331

This theorem is referenced by:  f1imacnv  5597  f1ococnv2  5607  fo00  5617  isoini  5954  isoselem  5956  f1opw2  6224  f1dmex  6273  bren  6912  f1oeng  6925  en1  6968  mapen  7027  ssenen  7032  phplem4  7036  phplem4on  7049  dif1en  7061  fiintim  7116  fidcenumlemim  7142  supisolem  7198  ordiso2  7225  djuunr  7256  omct  7307  ctssexmid  7340  1fv  10364  hashfacen  11090  fsumf1o  11941  fisumss  11943  fprodf1o  12139  fprodssdc  12141  nninfct  12602  ennnfonelemrn  13030  ennnfonelemnn0  13033  ennnfonelemim  13035  exmidunben  13037  ctinfomlemom  13038  ctinfom  13039  qnnen  13042  enctlem  13043  ssomct  13056  xpsfrn  13423  imasmndf1  13527  imasgrpf1  13689  imasrngf1  13960  imasringf1  14068  znleval  14657  hmeontr  15027  hmeoimaf1o  15028  fsumdvdsmul  15705  subctctexmid  16537  domomsubct  16538  exmidsbthrlem  16562  sbthomlem  16565