Theorem f1of1 5579

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

Syntax hints:   → wi 4  –1-1→wf1 5321  –onto→wfo 5322  –1-1-onto→wf1o 5323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-f1o 5331

This theorem is referenced by:  f1of  5580  f1sng  5623  f1oresrab  5808  f1ocnvfvrneq  5918  isores3  5951  isoini2  5955  f1oiso  5962  f1opw2  6224  tposf12  6430  enssdom  6930  mapen  7027  ssenen  7032  phplem4  7036  phplem4on  7049  fidceq  7051  en2eqpr  7092  fiintim  7116  f1finf1o  7137  preimaf1ofi  7141  isotilem  7196  inresflem  7250  casefun  7275  endjusym  7286  pr2cv1  7391  dju1p1e2  7398  frec2uzled  10681  iseqf1olemnab  10753  iseqf1olemab  10754  iseqf1olemnanb  10755  seqf1oglem1  10771  hashen  11036  hashfacen  11090  negfi  11779  fisumss  11943  fprodssdc  12141  phimullem  12787  eulerthlemh  12793  ctinfom  13039  ssnnctlemct  13057  f1ocpbllem  13383  f1ovscpbl  13385  xpsff1o2  13424  eqgen  13804  conjsubgen  13855  hmeoopn  15025  hmeocld  15026  hmeontr  15027  hmeoimaf1o  15028  usgrf1  16014  uspgr2wlkeq  16162  trlres  16185  iswomninnlem  16589