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

Theorem f1of1 5156
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 4939 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
21simplbi 268 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 4929   -onto->wfo 4930   -1-1-onto->wf1o 4931
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-f1o 4939
This theorem is referenced by:  f1of  5157  f1oresrab  5361  f1ocnvfvrneq  5453  isores3  5486  isoini2  5489  f1oiso  5496  f1opw2  5737  tposf12  5918  enssdom  6309  phplem4  6390  phplem4on  6402  fidceq  6404  en2eqpr  6434  isotilem  6478  frec2uzled  9511  sizeen  9808  negfi  10248
  Copyright terms: Public domain W3C validator