I've recently read some of the article on first order logic from http://mathworld.wolfram.com/First-OrderLogic.html and I'm puzzled by the explanation of universal instantiation that the author gives. It says
the following rule holds provided that F(r) is the result of substituting variable r for the free occurrences of x in sentential formula F and all occurrences of r resulting from this substitution are free in F,
∀x F(x) ------- F(r)
I don't understand how F(r) is the result of substituting variable r for the free occurrences of x when x is bound by the universal quantifier. How exactly is x free?