Theorem f1of1 5500

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

Syntax hints:   → wi 4  –1-1→wf1 5252  –onto→wfo 5253  –1-1-onto→wf1o 5254

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 5262

This theorem is referenced by:  f1of  5501  f1sng  5543  f1oresrab  5724  f1ocnvfvrneq  5826  isores3  5859  isoini2  5863  f1oiso  5870  f1opw2  6126  tposf12  6324  enssdom  6818  mapen  6904  ssenen  6909  phplem4  6913  phplem4on  6925  fidceq  6927  en2eqpr  6965  fiintim  6987  f1finf1o  7008  preimaf1ofi  7012  isotilem  7067  inresflem  7121  casefun  7146  endjusym  7157  dju1p1e2  7259  frec2uzled  10503  iseqf1olemnab  10575  iseqf1olemab  10576  iseqf1olemnanb  10577  seqf1oglem1  10593  hashen  10858  hashfacen  10910  negfi  11374  fisumss  11538  fprodssdc  11736  phimullem  12366  eulerthlemh  12372  ctinfom  12588  ssnnctlemct  12606  f1ocpbllem  12896  f1ovscpbl  12898  xpsff1o2  12937  eqgen  13300  conjsubgen  13351  hmeoopn  14490  hmeocld  14491  hmeontr  14492  hmeoimaf1o  14493  iswomninnlem  15609