[FOM] Question about "fresh" variables/objects in logics

[Divianszky Peter]

Does anybody know of a formal description of the concept of "fresh" 
variable/object in logic?

This concept is used in theoretical computer science quite often, but I 
have never seen a formal description of it.
Informally it could be descibed as:

Let X be an infinite set.
The definition
   x in X is fresh
means that
   x is an element of X
  and
   for all y in X defined elsewhere: x not equal y

The formal description of this concept would help me a lot. I am doing 
research in functional programming and I could use it there.

Peter Divianszky