Theorem f1ofo 5507

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

Syntax hints:   → wi 4  ^◡ccnv 4658  Fun wfun 5248  –onto→wfo 5252  –1-1-onto→wf1o 5253

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166  df-f 5258  df-f1 5259  df-fo 5260  df-f1o 5261

This theorem is referenced by:  f1imacnv  5517  f1ococnv2  5527  fo00  5536  isoini  5861  isoselem  5863  f1opw2  6124  f1dmex  6168  bren  6801  f1oeng  6811  en1  6853  mapen  6902  ssenen  6907  phplem4  6911  phplem4on  6923  dif1en  6935  fiintim  6985  fidcenumlemim  7011  supisolem  7067  ordiso2  7094  djuunr  7125  omct  7176  ctssexmid  7209  1fv  10205  hashfacen  10907  fsumf1o  11533  fisumss  11535  fprodf1o  11731  fprodssdc  11733  nninfct  12178  ennnfonelemrn  12576  ennnfonelemnn0  12579  ennnfonelemim  12581  exmidunben  12583  ctinfomlemom  12584  ctinfom  12585  qnnen  12588  enctlem  12589  ssomct  12602  xpsfrn  12933  imasgrpf1  13182  imasrngf1  13453  imasringf1  13561  znleval  14141  hmeontr  14481  hmeoimaf1o  14482  subctctexmid  15491  exmidsbthrlem  15512  sbthomlem  15515