Universal elimination

In symbolic logic, a valid inference in a system of quantifier rules. In a proof sequence, a universal quantifier is removed, and the variables bound by it are replaced with an individual constant. (In some systems, the quantifier is removed, and the variables are left unbound.)