Theorem f1ofo 5449

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

Syntax hints:   → wi 4  ^◡ccnv 4610  Fun wfun 5192  –onto→wfo 5196  –1-1-onto→wf1o 5197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205

This theorem is referenced by:  f1imacnv  5459  f1ococnv2  5469  fo00  5478  isoini  5797  isoselem  5799  f1opw2  6055  f1dmex  6095  bren  6725  f1oeng  6735  en1  6777  mapen  6824  ssenen  6829  phplem4  6833  phplem4on  6845  dif1en  6857  fiintim  6906  fidcenumlemim  6929  supisolem  6985  ordiso2  7012  djuunr  7043  omct  7094  ctssexmid  7126  1fv  10095  hashfacen  10771  fsumf1o  11353  fisumss  11355  fprodf1o  11551  fprodssdc  11553  ennnfonelemrn  12374  ennnfonelemnn0  12377  ennnfonelemim  12379  exmidunben  12381  ctinfomlemom  12382  ctinfom  12383  qnnen  12386  enctlem  12387  ssomct  12400  hmeontr  13107  hmeoimaf1o  13108  subctctexmid  14034  exmidsbthrlem  14054  sbthomlem  14057