Theorem f1of1 5543

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 5297	. 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 5287   -onto->wfo 5288   -1-1-onto->wf1o 5289

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 5297

This theorem is referenced by:  f1of  5544  f1sng  5587  f1oresrab  5768  f1ocnvfvrneq  5874  isores3  5907  isoini2  5911  f1oiso  5918  f1opw2  6175  tposf12  6378  enssdom  6876  mapen  6968  ssenen  6973  phplem4  6977  phplem4on  6990  fidceq  6992  en2eqpr  7030  fiintim  7054  f1finf1o  7075  preimaf1ofi  7079  isotilem  7134  inresflem  7188  casefun  7213  endjusym  7224  pr2cv1  7329  dju1p1e2  7336  frec2uzled  10611  iseqf1olemnab  10683  iseqf1olemab  10684  iseqf1olemnanb  10685  seqf1oglem1  10701  hashen  10966  hashfacen  11018  negfi  11654  fisumss  11818  fprodssdc  12016  phimullem  12662  eulerthlemh  12668  ctinfom  12914  ssnnctlemct  12932  f1ocpbllem  13257  f1ovscpbl  13259  xpsff1o2  13298  eqgen  13678  conjsubgen  13729  hmeoopn  14898  hmeocld  14899  hmeontr  14900  hmeoimaf1o  14901  iswomninnlem  16190