Theorem f1of1 5591

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 5340	. 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 5330   -onto->wfo 5331   -1-1-onto->wf1o 5332

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 5340

This theorem is referenced by:  f1of  5592  f1sng  5636  f1oresrab  5820  f1ocnvfvrneq  5933  isores3  5966  isoini2  5970  f1oiso  5977  f1opw2  6239  tposf12  6478  enssdom  6978  mapen  7075  ssenen  7080  phplem4  7084  phplem4on  7097  fidceq  7099  en2eqpr  7142  fiintim  7166  f1finf1o  7189  preimaf1ofi  7193  fsuppcorn  7226  isotilem  7265  inresflem  7319  casefun  7344  endjusym  7355  pr2cv1  7460  dju1p1e2  7468  frec2uzled  10754  iseqf1olemnab  10826  iseqf1olemab  10827  iseqf1olemnanb  10828  seqf1oglem1  10844  hashen  11109  hashfacen  11163  negfi  11868  fisumss  12033  fprodssdc  12231  phimullem  12877  eulerthlemh  12883  ctinfom  13129  ssnnctlemct  13147  f1ocpbllem  13473  f1ovscpbl  13475  xpsff1o2  13514  eqgen  13894  conjsubgen  13945  hmeoopn  15122  hmeocld  15123  hmeontr  15124  hmeoimaf1o  15125  usgrf1  16116  uspgr2wlkeq  16306  trlres  16331  iswomninnlem  16782