Theorem f1of1 5638

Description: A one-to-one onto mapping is a one-to-one mapping. (Contributed by NM, 12-Dec-2003.)

Assertion

Ref	Expression
f1of1	⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)

Proof of Theorem f1of1

Step	Hyp	Ref	Expression
1		df-f1o 5384	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
2	1	simplbi 274	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)

This proof depends on syntax axioms:   → wi 4  –1-1→wf1 5374  –onto→wfo 5375  –1-1-onto→wf1o 5376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f1o 5384

This theorem is used by:  f1of  5639  f1sng  5683  f1oresrab  5873  f1ocnvfvrneq  5988  isores3  6021  isoini2  6025  f1oiso  6032  f1opw2  6296  tposf12  6540  enssdom  7048  mapen  7146  ssenen  7152  phplem4  7156  phplem4on  7169  fidceq  7171  en2eqpr  7214  fiintim  7238  f1finf1o  7264  preimaf1ofi  7268  fsuppcorn  7301  isotilem  7346  inresflem  7400  casefun  7425  endjusym  7436  pr2cv1  7541  dju1p1e2  7549  frec2uzled  10866  iseqf1olemnab  10938  iseqf1olemab  10939  iseqf1olemnanb  10940  seqf1oglem1  10956  hashen  11223  hashfacen  11284  hashf1lem1  11285  negfi  11994  fisumss  12159  fprodssdc  12357  phimullem  13003  eulerthlemh  13009  ballotfilemscr  13262  ballotfilemro  13266  ballotfilemfrc  13270  ballotfilemrinv0  13276  ctinfom  13319  ssnnctlemct  13337  f1ocpbllem  13631  f1ovscpbl  13633  xpsff1o2  13672  eqgen  14030  conjsubgen  14081  hmeoopn  15412  hmeocld  15413  hmeontr  15414  hmeoimaf1o  15415  usgrf1  16416  uspgr2wlkeq  16606  trlres  16631  iswomninnlem  17099