Theorem f1of1 5520

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

Syntax hints:   → wi 4  –1-1→wf1 5267  –onto→wfo 5268  –1-1-onto→wf1o 5269

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 5277

This theorem is referenced by:  f1of  5521  f1sng  5563  f1oresrab  5744  f1ocnvfvrneq  5850  isores3  5883  isoini2  5887  f1oiso  5894  f1opw2  6151  tposf12  6354  enssdom  6852  mapen  6942  ssenen  6947  phplem4  6951  phplem4on  6963  fidceq  6965  en2eqpr  7003  fiintim  7027  f1finf1o  7048  preimaf1ofi  7052  isotilem  7107  inresflem  7161  casefun  7186  endjusym  7197  dju1p1e2  7304  frec2uzled  10572  iseqf1olemnab  10644  iseqf1olemab  10645  iseqf1olemnanb  10646  seqf1oglem1  10662  hashen  10927  hashfacen  10979  negfi  11481  fisumss  11645  fprodssdc  11843  phimullem  12489  eulerthlemh  12495  ctinfom  12741  ssnnctlemct  12759  f1ocpbllem  13084  f1ovscpbl  13086  xpsff1o2  13125  eqgen  13505  conjsubgen  13556  hmeoopn  14725  hmeocld  14726  hmeontr  14727  hmeoimaf1o  14728  iswomninnlem  15921