Theorem f1of1 5441

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 5205	. 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 5195   -onto->wfo 5196   -1-1-onto->wf1o 5197

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 5205

This theorem is referenced by:  f1of  5442  f1sng  5484  f1oresrab  5661  f1ocnvfvrneq  5761  isores3  5794  isoini2  5798  f1oiso  5805  f1opw2  6055  tposf12  6248  enssdom  6740  mapen  6824  ssenen  6829  phplem4  6833  phplem4on  6845  fidceq  6847  en2eqpr  6885  fiintim  6906  f1finf1o  6924  preimaf1ofi  6928  isotilem  6983  inresflem  7037  casefun  7062  endjusym  7073  dju1p1e2  7174  frec2uzled  10385  iseqf1olemnab  10444  iseqf1olemab  10445  iseqf1olemnanb  10446  hashen  10718  hashfacen  10771  negfi  11191  fisumss  11355  fprodssdc  11553  phimullem  12179  eulerthlemh  12185  ctinfom  12383  ssnnctlemct  12401  hmeoopn  13105  hmeocld  13106  hmeontr  13107  hmeoimaf1o  13108  iswomninnlem  14081