Theorem f1of1 5571

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  5572  f1sng  5615  f1oresrab  5800  f1ocnvfvrneq  5906  isores3  5939  isoini2  5943  f1oiso  5950  f1opw2  6212  tposf12  6415  enssdom  6913  mapen  7007  ssenen  7012  phplem4  7016  phplem4on  7029  fidceq  7031  en2eqpr  7069  fiintim  7093  f1finf1o  7114  preimaf1ofi  7118  isotilem  7173  inresflem  7227  casefun  7252  endjusym  7263  pr2cv1  7368  dju1p1e2  7375  frec2uzled  10651  iseqf1olemnab  10723  iseqf1olemab  10724  iseqf1olemnanb  10725  seqf1oglem1  10741  hashen  11006  hashfacen  11058  negfi  11739  fisumss  11903  fprodssdc  12101  phimullem  12747  eulerthlemh  12753  ctinfom  12999  ssnnctlemct  13017  f1ocpbllem  13343  f1ovscpbl  13345  xpsff1o2  13384  eqgen  13764  conjsubgen  13815  hmeoopn  14985  hmeocld  14986  hmeontr  14987  hmeoimaf1o  14988  usgrf1  15973  uspgr2wlkeq  16076  iswomninnlem  16417