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  7034  f1oeng  7047  en1  7090  mapen  7150  ssenen  7156  phplem4  7160  phplem4on  7173  dif1en  7187  fiintim  7242  fidcenumlemim  7274  supisolem  7354  ordiso2  7381  djuunr  7412  omct  7463  ctssexmid  7496  1fv  10563  hashfacen  11306  fsumf1o  12182  fisumss  12184  fprodf1o  12380  fprodssdc  12382  nninfct  12843  ballotfilemro  13324  ennnfonelemrn  13368  ennnfonelemnn0  13371  ennnfonelemim  13373  exmidunben  13375  ctinfomlemom  13376  ctinfom  13377  qnnen  13380  enctlem  13381  ssomct  13394  xpsfrn  13730  imasmndf1  13820  imasgrpf1  13974  imasrngf1  14363  imasringf1  14479  znleval  15097  hmeontr  15539  hmeoimaf1o  15540  fsumdvdsmul  16285  eupthvdres  16921  subctctexmid  17235  domomsubct  17236  exmidsbthrlem  17273  sbthomlem  17276