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