Theorem f1of1 5582

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

Syntax hints:   → wi 4  –1-1→wf1 5323  –onto→wfo 5324  –1-1-onto→wf1o 5325

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 5333

This theorem is referenced by:  f1of  5583  f1sng  5627  f1oresrab  5812  f1ocnvfvrneq  5922  isores3  5955  isoini2  5959  f1oiso  5966  f1opw2  6228  tposf12  6434  enssdom  6934  mapen  7031  ssenen  7036  phplem4  7040  phplem4on  7053  fidceq  7055  en2eqpr  7098  fiintim  7122  f1finf1o  7145  preimaf1ofi  7149  isotilem  7204  inresflem  7258  casefun  7283  endjusym  7294  pr2cv1  7399  dju1p1e2  7407  frec2uzled  10690  iseqf1olemnab  10762  iseqf1olemab  10763  iseqf1olemnanb  10764  seqf1oglem1  10780  hashen  11045  hashfacen  11099  negfi  11788  fisumss  11952  fprodssdc  12150  phimullem  12796  eulerthlemh  12802  ctinfom  13048  ssnnctlemct  13066  f1ocpbllem  13392  f1ovscpbl  13394  xpsff1o2  13433  eqgen  13813  conjsubgen  13864  hmeoopn  15034  hmeocld  15035  hmeontr  15036  hmeoimaf1o  15037  usgrf1  16025  uspgr2wlkeq  16215  trlres  16240  iswomninnlem  16653