Theorem f1ofo 5514

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

Syntax hints:   → wi 4  ^◡ccnv 4663  Fun wfun 5253  –onto→wfo 5257  –1-1-onto→wf1o 5258

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170  df-f 5263  df-f1 5264  df-fo 5265  df-f1o 5266

This theorem is referenced by:  f1imacnv  5524  f1ococnv2  5534  fo00  5543  isoini  5868  isoselem  5870  f1opw2  6133  f1dmex  6182  bren  6815  f1oeng  6825  en1  6867  mapen  6916  ssenen  6921  phplem4  6925  phplem4on  6937  dif1en  6949  fiintim  7001  fidcenumlemim  7027  supisolem  7083  ordiso2  7110  djuunr  7141  omct  7192  ctssexmid  7225  1fv  10233  hashfacen  10947  fsumf1o  11574  fisumss  11576  fprodf1o  11772  fprodssdc  11774  nninfct  12235  ennnfonelemrn  12663  ennnfonelemnn0  12666  ennnfonelemim  12668  exmidunben  12670  ctinfomlemom  12671  ctinfom  12672  qnnen  12675  enctlem  12676  ssomct  12689  xpsfrn  13054  imasmndf1  13158  imasgrpf1  13320  imasrngf1  13591  imasringf1  13699  znleval  14287  hmeontr  14657  hmeoimaf1o  14658  fsumdvdsmul  15335  subctctexmid  15755  domomsubct  15756  exmidsbthrlem  15779  sbthomlem  15782