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  11510  fisumss  11674  fprodssdc  11872  phimullem  12518  eulerthlemh  12524  ctinfom  12770  ssnnctlemct  12788  f1ocpbllem  13113  f1ovscpbl  13115  xpsff1o2  13154  eqgen  13534  conjsubgen  13585  hmeoopn  14754  hmeocld  14755  hmeontr  14756  hmeoimaf1o  14757  iswomninnlem  15950