ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  f1of1 Unicode version

Theorem f1of1 5456
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
StepHypRef Expression
1 df-f1o 5219 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
21simplbi 274 1  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   -1-1->wf1 5209   -onto->wfo 5210   -1-1-onto->wf1o 5211
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 5219
This theorem is referenced by:  f1of  5457  f1sng  5499  f1oresrab  5677  f1ocnvfvrneq  5777  isores3  5810  isoini2  5814  f1oiso  5821  f1opw2  6071  tposf12  6264  enssdom  6756  mapen  6840  ssenen  6845  phplem4  6849  phplem4on  6861  fidceq  6863  en2eqpr  6901  fiintim  6922  f1finf1o  6940  preimaf1ofi  6944  isotilem  6999  inresflem  7053  casefun  7078  endjusym  7089  dju1p1e2  7190  frec2uzled  10412  iseqf1olemnab  10471  iseqf1olemab  10472  iseqf1olemnanb  10473  hashen  10745  hashfacen  10797  negfi  11217  fisumss  11381  fprodssdc  11579  phimullem  12205  eulerthlemh  12211  ctinfom  12409  ssnnctlemct  12427  hmeoopn  13471  hmeocld  13472  hmeontr  13473  hmeoimaf1o  13474  iswomninnlem  14446
  Copyright terms: Public domain W3C validator