Theorem f1of1 5573

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

Syntax hints:   → wi 4  –1-1→wf1 5315  –onto→wfo 5316  –1-1-onto→wf1o 5317

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 5325

This theorem is referenced by:  f1of  5574  f1sng  5617  f1oresrab  5802  f1ocnvfvrneq  5912  isores3  5945  isoini2  5949  f1oiso  5956  f1opw2  6218  tposf12  6421  enssdom  6921  mapen  7015  ssenen  7020  phplem4  7024  phplem4on  7037  fidceq  7039  en2eqpr  7080  fiintim  7104  f1finf1o  7125  preimaf1ofi  7129  isotilem  7184  inresflem  7238  casefun  7263  endjusym  7274  pr2cv1  7379  dju1p1e2  7386  frec2uzled  10663  iseqf1olemnab  10735  iseqf1olemab  10736  iseqf1olemnanb  10737  seqf1oglem1  10753  hashen  11018  hashfacen  11071  negfi  11754  fisumss  11918  fprodssdc  12116  phimullem  12762  eulerthlemh  12768  ctinfom  13014  ssnnctlemct  13032  f1ocpbllem  13358  f1ovscpbl  13360  xpsff1o2  13399  eqgen  13779  conjsubgen  13830  hmeoopn  15000  hmeocld  15001  hmeontr  15002  hmeoimaf1o  15003  usgrf1  15988  uspgr2wlkeq  16106  trlres  16128  iswomninnlem  16477