Theorem f1ofo 5581

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

Syntax hints:   → wi 4  ^◡ccnv 4718  Fun wfun 5312  –onto→wfo 5316  –1-1-onto→wf1o 5317

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210  df-f 5322  df-f1 5323  df-fo 5324  df-f1o 5325

This theorem is referenced by:  f1imacnv  5591  f1ococnv2  5601  fo00  5611  isoini  5948  isoselem  5950  f1opw2  6218  f1dmex  6267  bren  6903  f1oeng  6916  en1  6959  mapen  7015  ssenen  7020  phplem4  7024  phplem4on  7037  dif1en  7049  fiintim  7104  fidcenumlemim  7130  supisolem  7186  ordiso2  7213  djuunr  7244  omct  7295  ctssexmid  7328  1fv  10347  hashfacen  11071  fsumf1o  11916  fisumss  11918  fprodf1o  12114  fprodssdc  12116  nninfct  12577  ennnfonelemrn  13005  ennnfonelemnn0  13008  ennnfonelemim  13010  exmidunben  13012  ctinfomlemom  13013  ctinfom  13014  qnnen  13017  enctlem  13018  ssomct  13031  xpsfrn  13398  imasmndf1  13502  imasgrpf1  13664  imasrngf1  13935  imasringf1  14043  znleval  14632  hmeontr  15002  hmeoimaf1o  15003  fsumdvdsmul  15680  subctctexmid  16425  domomsubct  16426  exmidsbthrlem  16450  sbthomlem  16453