Universal instantiation

In logic Universal instantiation (UI) is an inference from a truth about each member of a class of individuals to the truth about a particular individual of that class. It is generally given as a quantification rule for the universal quantifier but it can also be encoded in an axiom. It is one of the basic principles used in quantification theory.

Example: "All dogs are mammals. Therefore Fido is a mammal."

In symbols the rule as an axiom schema is:

∀xA → A(a/x), for some term a and where A(a/x) is the result of substituting a for all free occurrences of x in A.

And as a rule of inference it is:

from ⊢ ∀xA infer ⊢ A(a/x), with A(a/x) the same as above.