Theorem f1ofo 5480

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

Syntax hints:   → wi 4  ^◡ccnv 4637  Fun wfun 5222  –onto→wfo 5226  –1-1-onto→wf1o 5227

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-3an 981  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-in 3147  df-ss 3154  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235

This theorem is referenced by:  f1imacnv  5490  f1ococnv2  5500  fo00  5509  isoini  5832  isoselem  5834  f1opw2  6091  f1dmex  6131  bren  6761  f1oeng  6771  en1  6813  mapen  6860  ssenen  6865  phplem4  6869  phplem4on  6881  dif1en  6893  fiintim  6942  fidcenumlemim  6965  supisolem  7021  ordiso2  7048  djuunr  7079  omct  7130  ctssexmid  7162  1fv  10153  hashfacen  10830  fsumf1o  11412  fisumss  11414  fprodf1o  11610  fprodssdc  11612  ennnfonelemrn  12434  ennnfonelemnn0  12437  ennnfonelemim  12439  exmidunben  12441  ctinfomlemom  12442  ctinfom  12443  qnnen  12446  enctlem  12447  ssomct  12460  xpsfrn  12788  imasgrpf1  13007  imasrngf1  13209  imasringf1  13313  hmeontr  14109  hmeoimaf1o  14110  subctctexmid  15047  exmidsbthrlem  15067  sbthomlem  15070