Theorem f1of1 5461

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 5224	. 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 5214   -onto->wfo 5215   -1-1-onto->wf1o 5216

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 5224

This theorem is referenced by:  f1of  5462  f1sng  5504  f1oresrab  5682  f1ocnvfvrneq  5783  isores3  5816  isoini2  5820  f1oiso  5827  f1opw2  6077  tposf12  6270  enssdom  6762  mapen  6846  ssenen  6851  phplem4  6855  phplem4on  6867  fidceq  6869  en2eqpr  6907  fiintim  6928  f1finf1o  6946  preimaf1ofi  6950  isotilem  7005  inresflem  7059  casefun  7084  endjusym  7095  dju1p1e2  7196  frec2uzled  10429  iseqf1olemnab  10488  iseqf1olemab  10489  iseqf1olemnanb  10490  hashen  10764  hashfacen  10816  negfi  11236  fisumss  11400  fprodssdc  11598  phimullem  12225  eulerthlemh  12231  ctinfom  12429  ssnnctlemct  12447  f1ocpbllem  12731  f1ovscpbl  12733  xpsff1o2  12770  eqgen  13086  hmeoopn  13814  hmeocld  13815  hmeontr  13816  hmeoimaf1o  13817  iswomninnlem  14800