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	|- ( F : A -1-1-onto-> B -> F : A -1-1-> B )

Proof of Theorem f1of1

Step	Hyp	Ref	Expression
1		df-f1o 5325	. 2 |- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
2	1	simplbi 274	1 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )

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  11755  fisumss  11919  fprodssdc  12117  phimullem  12763  eulerthlemh  12769  ctinfom  13015  ssnnctlemct  13033  f1ocpbllem  13359  f1ovscpbl  13361  xpsff1o2  13400  eqgen  13780  conjsubgen  13831  hmeoopn  15001  hmeocld  15002  hmeontr  15003  hmeoimaf1o  15004  usgrf1  15989  uspgr2wlkeq  16111  trlres  16133  iswomninnlem  16505