Theorem f1of1 5638

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

This proof depends on syntax axioms:   → wi 4  –1-1→wf1 5374  –onto→wfo 5375  –1-1-onto→wf1o 5376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f1o 5384

This theorem is used by:  f1of  5639  f1sng  5683  f1oresrab  5873  f1ocnvfvrneq  5988  isores3  6021  isoini2  6025  f1oiso  6032  f1opw2  6296  tposf12  6540  enssdom  7048  mapen  7146  ssenen  7152  phplem4  7156  phplem4on  7169  fidceq  7171  en2eqpr  7214  fiintim  7238  f1finf1o  7264  preimaf1ofi  7268  fsuppcorn  7301  isotilem  7346  inresflem  7400  casefun  7425  endjusym  7436  pr2cv1  7541  dju1p1e2  7549  frec2uzled  10879  iseqf1olemnab  10951  iseqf1olemab  10952  iseqf1olemnanb  10953  seqf1oglem1  10969  hashen  11237  hashfacen  11298  hashf1lem1  11299  negfi  12009  fisumss  12175  fprodssdc  12373  phimullem  13023  eulerthlemh  13029  ballotfilemscr  13311  ballotfilemro  13315  ballotfilemfrc  13319  ballotfilemrinv0  13325  ctinfom  13368  ssnnctlemct  13386  f1ocpbllem  13680  f1ovscpbl  13682  xpsff1o2  13721  eqgen  14079  conjsubgen  14130  hmeoopn  15461  hmeocld  15462  hmeontr  15463  hmeoimaf1o  15464  usgrf1  16514  uspgr2wlkeq  16704  trlres  16729  iswomninnlem  17197