Theorem f1ofo 5626

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

Syntax hints:   → wi 4  ^◡ccnv 4753  Fun wfun 5351  –onto→wfo 5355  –1-1-onto→wf1o 5356

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227  df-f 5361  df-f1 5362  df-fo 5363  df-f1o 5364

This theorem is referenced by:  f1imacnv  5636  f1ococnv2  5646  fo00  5657  isoini  5997  isoselem  5999  f1opw2  6269  f1dmex  6318  bren  6996  f1oeng  7009  en1  7052  mapen  7112  ssenen  7118  phplem4  7122  phplem4on  7135  dif1en  7149  fiintim  7204  fidcenumlemim  7235  supisolem  7312  ordiso2  7339  djuunr  7370  omct  7421  ctssexmid  7454  1fv  10495  hashfacen  11233  fsumf1o  12101  fisumss  12103  fprodf1o  12299  fprodssdc  12301  nninfct  12762  ballotfilemro  13210  ennnfonelemrn  13254  ennnfonelemnn0  13257  ennnfonelemim  13259  exmidunben  13261  ctinfomlemom  13262  ctinfom  13263  qnnen  13266  enctlem  13267  ssomct  13280  xpsfrn  13614  imasmndf1  13709  imasgrpf1  13865  imasrngf1  14196  imasringf1  14308  znleval  14927  hmeontr  15304  hmeoimaf1o  15305  fsumdvdsmul  15985  eupthvdres  16596  subctctexmid  16900  domomsubct  16901  exmidsbthrlem  16928  sbthomlem  16931