Description: Formula-building rule for restricted universal quantifier (deduction form). For a version based on fewer axioms see ralbidv . (Contributed by NM, 27-Jun-1998)