Description: Rule used to change the bound variable in a restricted universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017)