Theorem f1of1 5613

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 5359	. 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 5349   -onto->wfo 5350   -1-1-onto->wf1o 5351

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 5359

This theorem is referenced by:  f1of  5614  f1sng  5658  f1oresrab  5842  f1ocnvfvrneq  5955  isores3  5988  isoini2  5992  f1oiso  5999  f1opw2  6261  tposf12  6500  enssdom  7001  mapen  7099  ssenen  7105  phplem4  7109  phplem4on  7122  fidceq  7124  en2eqpr  7167  fiintim  7191  f1finf1o  7217  preimaf1ofi  7221  fsuppcorn  7254  isotilem  7297  inresflem  7351  casefun  7376  endjusym  7387  pr2cv1  7492  dju1p1e2  7500  frec2uzled  10791  iseqf1olemnab  10863  iseqf1olemab  10864  iseqf1olemnanb  10865  seqf1oglem1  10881  hashen  11147  hashfacen  11208  negfi  11913  fisumss  12078  fprodssdc  12276  phimullem  12922  eulerthlemh  12928  ctinfom  13179  ssnnctlemct  13197  f1ocpbllem  13523  f1ovscpbl  13525  xpsff1o2  13564  eqgen  13944  conjsubgen  13995  hmeoopn  15176  hmeocld  15177  hmeontr  15178  hmeoimaf1o  15179  usgrf1  16170  uspgr2wlkeq  16360  trlres  16385  iswomninnlem  16834