Theorem f1of1 5641

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 5387	. 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 5377  –onto→wfo 5378  –1-1-onto→wf1o 5379

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 5387

This theorem is used by:  f1of  5642  f1sng  5686  f1oresrab  5876  f1ocnvfvrneq  5991  isores3  6024  isoini2  6028  f1oiso  6035  f1opw2  6299  tposf12  6544  enssdom  7052  mapen  7150  ssenen  7156  phplem4  7160  phplem4on  7173  fidceq  7175  en2eqpr  7218  fiintim  7242  f1finf1o  7269  preimaf1ofi  7273  fsuppcorn  7306  isotilem  7352  inresflem  7406  casefun  7431  endjusym  7442  pr2cv1  7547  dju1p1e2  7555  frec2uzled  10887  iseqf1olemnab  10959  iseqf1olemab  10960  iseqf1olemnanb  10961  seqf1oglem1  10977  hashen  11245  hashfacen  11306  hashf1lem1  11307  negfi  12017  fisumss  12184  fprodssdc  12382  phimullem  13032  eulerthlemh  13038  ballotfilemscr  13320  ballotfilemro  13324  ballotfilemfrc  13328  ballotfilemrinv0  13334  ctinfom  13377  ssnnctlemct  13395  f1ocpbllem  13690  f1ovscpbl  13692  xpsff1o2  13731  eqgen  14089  conjsubgen  14140  hmeoopn  15537  hmeocld  15538  hmeontr  15539  hmeoimaf1o  15540  usgrf1  16621  uspgr2wlkeq  16811  trlres  16836  iswomninnlem  17306