Theorem f1of1 5641

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 5387	. 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 )

This proof depends on syntax axioms:   -> wi 4   -1-1->wf1 5377   -onto->wfo 5378   -1-1-onto->wf1o 5379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f1o 5387

This theorem is used by:  f1of  5642  f1sng  5686  f1oresrab  5876  f1ocnvfvrneq  5991  isores3  6024  isoini2  6028  f1oiso  6035  f1opw2  6299  tposf12  6545  enssdom  7054  mapen  7152  ssenen  7158  phplem4  7162  phplem4on  7175  fidceq  7177  en2eqpr  7220  fiintim  7244  f1finf1o  7271  preimaf1ofi  7275  isotilem  7352  inresflem  7406  casefun  7431  endjusym  7442  pr2cv1  7547  dju1p1e2  7555  frec2uzled  10886  iseqf1olemnab  10958  iseqf1olemab  10959  iseqf1olemnanb  10960  seqf1oglem1  10976  hashen  11244  hashfacen  11305  hashf1lem1  11306  negfi  12016  fisumss  12183  fprodssdc  12381  phimullem  13031  eulerthlemh  13037  ballotfilemscr  13319  ballotfilemro  13323  ballotfilemfrc  13327  ballotfilemrinv0  13333  ctinfom  13376  ssnnctlemct  13394  f1ocpbllem  13689  f1ovscpbl  13691  xpsff1o2  13730  eqgen  14088  conjsubgen  14139  hmeoopn  15554  hmeocld  15555  hmeontr  15556  hmeoimaf1o  15557  usgrf1  16638  uspgr2wlkeq  16828  trlres  16853  iswomninnlem  17323