With[x = , y = , ... , expr] specifies that in expr occurrences of the symbols x, y, ... should be replaced by , , ... .
With allows you to define local constants.
With replaces symbols in expr only when they do not occur as local variables inside scoping constructs.
You can use With[vars, body /; cond] as the right-hand side of a transformation rule with a condition attached.
With has attribute HoldAll.
With is a scoping construct (see Section A.3.8).
With constructs can be nested in any way.
With implements read-only lexical variables.
See The Mathematica Book: Section 2.6.2.
See also: Module, Block, ReplaceAll.