Theorem f1of1 5506

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 5266	. 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 5256   -onto->wfo 5257   -1-1-onto->wf1o 5258

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 5266

This theorem is referenced by:  f1of  5507  f1sng  5549  f1oresrab  5730  f1ocnvfvrneq  5832  isores3  5865  isoini2  5869  f1oiso  5876  f1opw2  6133  tposf12  6336  enssdom  6830  mapen  6916  ssenen  6921  phplem4  6925  phplem4on  6937  fidceq  6939  en2eqpr  6977  fiintim  7001  f1finf1o  7022  preimaf1ofi  7026  isotilem  7081  inresflem  7135  casefun  7160  endjusym  7171  dju1p1e2  7276  frec2uzled  10538  iseqf1olemnab  10610  iseqf1olemab  10611  iseqf1olemnanb  10612  seqf1oglem1  10628  hashen  10893  hashfacen  10945  negfi  11410  fisumss  11574  fprodssdc  11772  phimullem  12418  eulerthlemh  12424  ctinfom  12670  ssnnctlemct  12688  f1ocpbllem  13012  f1ovscpbl  13014  xpsff1o2  13053  eqgen  13433  conjsubgen  13484  hmeoopn  14631  hmeocld  14632  hmeontr  14633  hmeoimaf1o  14634  iswomninnlem  15780