UNIVERSAL INSTANTIATION

In logic 'universal instantiation' ('UI', also called "Dictum de omni") 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. Fido is a dog. Therefore Fido is a mammal."
In symbols the rule as an axiom schema is
:
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 ⊢ ∀''x'' ''A'' infer ⊢ ''A''(''a''/''x''),
with ''A''(''a''/''x'') the same as above.