Theorem f1ofo 5295

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

Syntax hints:   → wi 4  ^◡ccnv 4466  Fun wfun 5043  –onto→wfo 5047  –1-1-onto→wf1o 5048

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-11 1449  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-3an 929  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-in 3019  df-ss 3026  df-f 5053  df-f1 5054  df-fo 5055  df-f1o 5056

This theorem is referenced by:  f1imacnv  5305  f1ococnv2  5315  fo00  5324  isoini  5635  isoselem  5637  f1opw2  5888  f1dmex  5925  bren  6544  f1oeng  6554  en1  6596  mapen  6642  ssenen  6647  phplem4  6651  phplem4on  6663  dif1en  6675  fiintim  6719  fidcenumlemim  6741  supisolem  6783  ordiso2  6808  djuunr  6838  1fv  9699  hashfacen  10356  fsumf1o  10933  fisumss  10935  exmidsbthrlem  12617