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

Theorem f1of1 5359
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 5125 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
21simplbi 272 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 5115   -onto->wfo 5116   -1-1-onto->wf1o 5117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-f1o 5125
This theorem is referenced by:  f1of  5360  f1sng  5402  f1oresrab  5578  f1ocnvfvrneq  5676  isores3  5709  isoini2  5713  f1oiso  5720  f1opw2  5969  tposf12  6159  enssdom  6649  mapen  6733  ssenen  6738  phplem4  6742  phplem4on  6754  fidceq  6756  en2eqpr  6794  fiintim  6810  f1finf1o  6828  preimaf1ofi  6832  isotilem  6886  inresflem  6938  casefun  6963  endjusym  6974  dju1p1e2  7046  frec2uzled  10195  iseqf1olemnab  10254  iseqf1olemab  10255  iseqf1olemnanb  10256  hashen  10523  hashfacen  10572  negfi  10992  fisumss  11154  phimullem  11890  ctinfom  11930  hmeoopn  12469  hmeocld  12470  hmeontr  12471  hmeoimaf1o  12472
  Copyright terms: Public domain W3C validator