Theorem f1ofo 5528

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

Syntax hints:   → wi 4  ^◡ccnv 4673  Fun wfun 5264  –onto→wfo 5268  –1-1-onto→wf1o 5269

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178  df-f 5274  df-f1 5275  df-fo 5276  df-f1o 5277

This theorem is referenced by:  f1imacnv  5538  f1ococnv2  5548  fo00  5557  isoini  5886  isoselem  5888  f1opw2  6151  f1dmex  6200  bren  6834  f1oeng  6847  en1  6890  mapen  6942  ssenen  6947  phplem4  6951  phplem4on  6963  dif1en  6975  fiintim  7027  fidcenumlemim  7053  supisolem  7109  ordiso2  7136  djuunr  7167  omct  7218  ctssexmid  7251  1fv  10260  hashfacen  10979  fsumf1o  11672  fisumss  11674  fprodf1o  11870  fprodssdc  11872  nninfct  12333  ennnfonelemrn  12761  ennnfonelemnn0  12764  ennnfonelemim  12766  exmidunben  12768  ctinfomlemom  12769  ctinfom  12770  qnnen  12773  enctlem  12774  ssomct  12787  xpsfrn  13153  imasmndf1  13257  imasgrpf1  13419  imasrngf1  13690  imasringf1  13798  znleval  14386  hmeontr  14756  hmeoimaf1o  14757  fsumdvdsmul  15434  subctctexmid  15899  domomsubct  15900  exmidsbthrlem  15923  sbthomlem  15926