Theorem f1of1 5406

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 5170	. 2 |- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
2	1	simplbi 272	1 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )

Syntax hints:   -> wi 4   -1-1->wf1 5160   -onto->wfo 5161   -1-1-onto->wf1o 5162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-f1o 5170

This theorem is referenced by:  f1of  5407  f1sng  5449  f1oresrab  5625  f1ocnvfvrneq  5723  isores3  5756  isoini2  5760  f1oiso  5767  f1opw2  6016  tposf12  6206  enssdom  6696  mapen  6780  ssenen  6785  phplem4  6789  phplem4on  6801  fidceq  6803  en2eqpr  6841  fiintim  6862  f1finf1o  6880  preimaf1ofi  6884  isotilem  6938  inresflem  6990  casefun  7015  endjusym  7026  dju1p1e2  7111  frec2uzled  10306  iseqf1olemnab  10365  iseqf1olemab  10366  iseqf1olemnanb  10367  hashen  10635  hashfacen  10684  negfi  11104  fisumss  11266  fprodssdc  11464  phimullem  12068  ctinfom  12108  hmeoopn  12650  hmeocld  12651  hmeontr  12652  hmeoimaf1o  12653  iswomninnlem  13561