Theorem f1of1 5499

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

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

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 5261

This theorem is referenced by:  f1of  5500  f1sng  5542  f1oresrab  5723  f1ocnvfvrneq  5825  isores3  5858  isoini2  5862  f1oiso  5869  f1opw2  6124  tposf12  6322  enssdom  6816  mapen  6902  ssenen  6907  phplem4  6911  phplem4on  6923  fidceq  6925  en2eqpr  6963  fiintim  6985  f1finf1o  7006  preimaf1ofi  7010  isotilem  7065  inresflem  7119  casefun  7144  endjusym  7155  dju1p1e2  7257  frec2uzled  10500  iseqf1olemnab  10572  iseqf1olemab  10573  iseqf1olemnanb  10574  seqf1oglem1  10590  hashen  10855  hashfacen  10907  negfi  11371  fisumss  11535  fprodssdc  11733  phimullem  12363  eulerthlemh  12369  ctinfom  12585  ssnnctlemct  12603  f1ocpbllem  12893  f1ovscpbl  12895  xpsff1o2  12934  eqgen  13297  conjsubgen  13348  hmeoopn  14479  hmeocld  14480  hmeontr  14481  hmeoimaf1o  14482  iswomninnlem  15539