Theorem f1ofo 5578

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

Syntax hints:   → wi 4  ^◡ccnv 4717  Fun wfun 5311  –onto→wfo 5315  –1-1-onto→wf1o 5316

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 5321  df-f1 5322  df-fo 5323  df-f1o 5324

This theorem is referenced by:  f1imacnv  5588  f1ococnv2  5598  fo00  5608  isoini  5941  isoselem  5943  f1opw2  6210  f1dmex  6259  bren  6893  f1oeng  6906  en1  6949  mapen  7003  ssenen  7008  phplem4  7012  phplem4on  7025  dif1en  7037  fiintim  7089  fidcenumlemim  7115  supisolem  7171  ordiso2  7198  djuunr  7229  omct  7280  ctssexmid  7313  1fv  10331  hashfacen  11053  fsumf1o  11896  fisumss  11898  fprodf1o  12094  fprodssdc  12096  nninfct  12557  ennnfonelemrn  12985  ennnfonelemnn0  12988  ennnfonelemim  12990  exmidunben  12992  ctinfomlemom  12993  ctinfom  12994  qnnen  12997  enctlem  12998  ssomct  13011  xpsfrn  13378  imasmndf1  13482  imasgrpf1  13644  imasrngf1  13915  imasringf1  14023  znleval  14611  hmeontr  14981  hmeoimaf1o  14982  fsumdvdsmul  15659  subctctexmid  16325  domomsubct  16326  exmidsbthrlem  16349  sbthomlem  16352