Theorem f1of1 5570

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

Syntax hints:   → wi 4  –1-1→wf1 5314  –onto→wfo 5315  –1-1-onto→wf1o 5316

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 5324

This theorem is referenced by:  f1of  5571  f1sng  5614  f1oresrab  5799  f1ocnvfvrneq  5905  isores3  5938  isoini2  5942  f1oiso  5949  f1opw2  6210  tposf12  6413  enssdom  6911  mapen  7003  ssenen  7008  phplem4  7012  phplem4on  7025  fidceq  7027  en2eqpr  7065  fiintim  7089  f1finf1o  7110  preimaf1ofi  7114  isotilem  7169  inresflem  7223  casefun  7248  endjusym  7259  pr2cv1  7364  dju1p1e2  7371  frec2uzled  10646  iseqf1olemnab  10718  iseqf1olemab  10719  iseqf1olemnanb  10720  seqf1oglem1  10736  hashen  11001  hashfacen  11053  negfi  11734  fisumss  11898  fprodssdc  12096  phimullem  12742  eulerthlemh  12748  ctinfom  12994  ssnnctlemct  13012  f1ocpbllem  13338  f1ovscpbl  13340  xpsff1o2  13379  eqgen  13759  conjsubgen  13810  hmeoopn  14979  hmeocld  14980  hmeontr  14981  hmeoimaf1o  14982  usgrf1  15967  iswomninnlem  16376