Theorem f1of1 5430

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 5194	. 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 5184   -onto->wfo 5185   -1-1-onto->wf1o 5186

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 5194

This theorem is referenced by:  f1of  5431  f1sng  5473  f1oresrab  5649  f1ocnvfvrneq  5749  isores3  5782  isoini2  5786  f1oiso  5793  f1opw2  6043  tposf12  6233  enssdom  6724  mapen  6808  ssenen  6813  phplem4  6817  phplem4on  6829  fidceq  6831  en2eqpr  6869  fiintim  6890  f1finf1o  6908  preimaf1ofi  6912  isotilem  6967  inresflem  7021  casefun  7046  endjusym  7057  dju1p1e2  7149  frec2uzled  10360  iseqf1olemnab  10419  iseqf1olemab  10420  iseqf1olemnanb  10421  hashen  10693  hashfacen  10745  negfi  11165  fisumss  11329  fprodssdc  11527  phimullem  12153  eulerthlemh  12159  ctinfom  12357  ssnnctlemct  12375  hmeoopn  12911  hmeocld  12912  hmeontr  12913  hmeoimaf1o  12914  iswomninnlem  13888