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  7347  inresflem  7401  casefun  7426  endjusym  7437  pr2cv1  7542  dju1p1e2  7550  frec2uzled  10881  iseqf1olemnab  10953  iseqf1olemab  10954  iseqf1olemnanb  10955  seqf1oglem1  10971  hashen  11239  hashfacen  11300  hashf1lem1  11301  negfi  12011  fisumss  12178  fprodssdc  12376  phimullem  13026  eulerthlemh  13032  ballotfilemscr  13314  ballotfilemro  13318  ballotfilemfrc  13322  ballotfilemrinv0  13328  ctinfom  13371  ssnnctlemct  13389  f1ocpbllem  13684  f1ovscpbl  13686  xpsff1o2  13725  eqgen  14083  conjsubgen  14134  hmeoopn  15503  hmeocld  15504  hmeontr  15505  hmeoimaf1o  15506  usgrf1  16582  uspgr2wlkeq  16772  trlres  16797  iswomninnlem  17266