Theorem f1ofo 5649

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

This proof depends on syntax axioms:   → wi 4  ^◡ccnv 4775  Fun wfun 5374  –onto→wfo 5378  –1-1-onto→wf1o 5379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233  df-f 5384  df-f1 5385  df-fo 5386  df-f1o 5387

This theorem is used by:  f1imacnv  5659  f1ococnv2  5669  fo00  5680  isoini  6027  isoselem  6029  f1opw2  6299  f1dmex  6349  bren  7036  f1oeng  7049  en1  7092  mapen  7152  ssenen  7158  phplem4  7162  phplem4on  7175  dif1en  7189  fiintim  7244  fidcenumlemim  7276  supisolem  7354  ordiso2  7381  djuunr  7412  omct  7463  ctssexmid  7496  1fv  10562  hashfacen  11305  fsumf1o  12181  fisumss  12183  fprodf1o  12379  fprodssdc  12381  nninfct  12842  ballotfilemro  13323  ennnfonelemrn  13367  ennnfonelemnn0  13370  ennnfonelemim  13372  exmidunben  13374  ctinfomlemom  13375  ctinfom  13376  qnnen  13379  enctlem  13380  ssomct  13393  xpsfrn  13729  imasmndf1  13819  imasgrpf1  13973  imasrngf1  14362  imasringf1  14478  znleval  15096  hmeontr  15556  hmeoimaf1o  15557  fsumdvdsmul  16302  eupthvdres  16938  subctctexmid  17252  domomsubct  17253  exmidsbthrlem  17290  sbthomlem  17293