Using \colon or : in formulas?

Both : and \colon typeset a colon, but \colon is a punctuation symbol, while : is considered as a relation symbol as regards to spacing.

The main use of : is in set descriptions

\{\, x : x \notin x \,\}

(somebody uses \mid for this, where a simple | would be wrong; thin spaces after \{ and before \} are recommended by Knuth, be consistent in using them or not).

Conversely, \colon should be used for mappings

f\colon A \to B

but unfortunately many writers don't make this distinction and use :, getting a wrong spacing.

The rule to follow is just the same: use \colon when it's a "punctuation colon", use : when it represents a relation between what's at its left and at its right. In something like "for all x:" I would consider the colon as punctuation, so \forall x\colon

Note that the amsmath package changes the definition of \colon so that it's not exactly the same as a punctuation symbol:

\renewcommand{\colon}{\nobreak\mskip2mu\mathpunct{}\nonscript
  \mkern-\thinmuskip{:}\mskip6muplus1mu\relax}

This adds a bit of space before the colon, which seems more right than with a simple \mathpunct.

If you're trying to typeset a variable-has-type colon in type theory, you want {:} or \mathord{:} (they display the same). For example, you'll get a nice looking STLC identity function with $\lambda x {:} A . x$.

See this page for a more general discussion.