Theorem f1ofo 5529

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

Syntax hints:   → wi 4  ^◡ccnv 4674  Fun wfun 5265  –onto→wfo 5269  –1-1-onto→wf1o 5270

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278

This theorem is referenced by:  f1imacnv  5539  f1ococnv2  5549  fo00  5558  isoini  5887  isoselem  5889  f1opw2  6152  f1dmex  6201  bren  6835  f1oeng  6848  en1  6891  mapen  6943  ssenen  6948  phplem4  6952  phplem4on  6964  dif1en  6976  fiintim  7028  fidcenumlemim  7054  supisolem  7110  ordiso2  7137  djuunr  7168  omct  7219  ctssexmid  7252  1fv  10261  hashfacen  10981  fsumf1o  11701  fisumss  11703  fprodf1o  11899  fprodssdc  11901  nninfct  12362  ennnfonelemrn  12790  ennnfonelemnn0  12793  ennnfonelemim  12795  exmidunben  12797  ctinfomlemom  12798  ctinfom  12799  qnnen  12802  enctlem  12803  ssomct  12816  xpsfrn  13182  imasmndf1  13286  imasgrpf1  13448  imasrngf1  13719  imasringf1  13827  znleval  14415  hmeontr  14785  hmeoimaf1o  14786  fsumdvdsmul  15463  subctctexmid  15937  domomsubct  15938  exmidsbthrlem  15961  sbthomlem  15964