Theorem f1of1 5503

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

Syntax hints:   → wi 4  –1-1→wf1 5255  –onto→wfo 5256  –1-1-onto→wf1o 5257

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 5265

This theorem is referenced by:  f1of  5504  f1sng  5546  f1oresrab  5727  f1ocnvfvrneq  5829  isores3  5862  isoini2  5866  f1oiso  5873  f1opw2  6129  tposf12  6327  enssdom  6821  mapen  6907  ssenen  6912  phplem4  6916  phplem4on  6928  fidceq  6930  en2eqpr  6968  fiintim  6992  f1finf1o  7013  preimaf1ofi  7017  isotilem  7072  inresflem  7126  casefun  7151  endjusym  7162  dju1p1e2  7264  frec2uzled  10521  iseqf1olemnab  10593  iseqf1olemab  10594  iseqf1olemnanb  10595  seqf1oglem1  10611  hashen  10876  hashfacen  10928  negfi  11393  fisumss  11557  fprodssdc  11755  phimullem  12393  eulerthlemh  12399  ctinfom  12645  ssnnctlemct  12663  f1ocpbllem  12953  f1ovscpbl  12955  xpsff1o2  12994  eqgen  13357  conjsubgen  13408  hmeoopn  14547  hmeocld  14548  hmeontr  14549  hmeoimaf1o  14550  iswomninnlem  15693