Theorem f1of1 5521

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 5278	. 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 5268   -onto->wfo 5269   -1-1-onto->wf1o 5270

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 5278

This theorem is referenced by:  f1of  5522  f1sng  5564  f1oresrab  5745  f1ocnvfvrneq  5851  isores3  5884  isoini2  5888  f1oiso  5895  f1opw2  6152  tposf12  6355  enssdom  6853  mapen  6943  ssenen  6948  phplem4  6952  phplem4on  6964  fidceq  6966  en2eqpr  7004  fiintim  7028  f1finf1o  7049  preimaf1ofi  7053  isotilem  7108  inresflem  7162  casefun  7187  endjusym  7198  dju1p1e2  7305  frec2uzled  10574  iseqf1olemnab  10646  iseqf1olemab  10647  iseqf1olemnanb  10648  seqf1oglem1  10664  hashen  10929  hashfacen  10981  negfi  11539  fisumss  11703  fprodssdc  11901  phimullem  12547  eulerthlemh  12553  ctinfom  12799  ssnnctlemct  12817  f1ocpbllem  13142  f1ovscpbl  13144  xpsff1o2  13183  eqgen  13563  conjsubgen  13614  hmeoopn  14783  hmeocld  14784  hmeontr  14785  hmeoimaf1o  14786  iswomninnlem  15988