Theorem f1of1 5506

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

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

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 5266

This theorem is referenced by:  f1of  5507  f1sng  5549  f1oresrab  5730  f1ocnvfvrneq  5832  isores3  5865  isoini2  5869  f1oiso  5876  f1opw2  6133  tposf12  6336  enssdom  6830  mapen  6916  ssenen  6921  phplem4  6925  phplem4on  6937  fidceq  6939  en2eqpr  6977  fiintim  7001  f1finf1o  7022  preimaf1ofi  7026  isotilem  7081  inresflem  7135  casefun  7160  endjusym  7171  dju1p1e2  7278  frec2uzled  10540  iseqf1olemnab  10612  iseqf1olemab  10613  iseqf1olemnanb  10614  seqf1oglem1  10630  hashen  10895  hashfacen  10947  negfi  11412  fisumss  11576  fprodssdc  11774  phimullem  12420  eulerthlemh  12426  ctinfom  12672  ssnnctlemct  12690  f1ocpbllem  13014  f1ovscpbl  13016  xpsff1o2  13055  eqgen  13435  conjsubgen  13486  hmeoopn  14655  hmeocld  14656  hmeontr  14657  hmeoimaf1o  14658  iswomninnlem  15806