Theorem f1of1 5523

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 5279	. 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 5269   -onto->wfo 5270   -1-1-onto->wf1o 5271

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 5279

This theorem is referenced by:  f1of  5524  f1sng  5566  f1oresrab  5747  f1ocnvfvrneq  5853  isores3  5886  isoini2  5890  f1oiso  5897  f1opw2  6154  tposf12  6357  enssdom  6855  mapen  6945  ssenen  6950  phplem4  6954  phplem4on  6966  fidceq  6968  en2eqpr  7006  fiintim  7030  f1finf1o  7051  preimaf1ofi  7055  isotilem  7110  inresflem  7164  casefun  7189  endjusym  7200  dju1p1e2  7307  frec2uzled  10576  iseqf1olemnab  10648  iseqf1olemab  10649  iseqf1olemnanb  10650  seqf1oglem1  10666  hashen  10931  hashfacen  10983  negfi  11572  fisumss  11736  fprodssdc  11934  phimullem  12580  eulerthlemh  12586  ctinfom  12832  ssnnctlemct  12850  f1ocpbllem  13175  f1ovscpbl  13177  xpsff1o2  13216  eqgen  13596  conjsubgen  13647  hmeoopn  14816  hmeocld  14817  hmeontr  14818  hmeoimaf1o  14819  iswomninnlem  16025