Description: Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017) (Proof shortened by Wolf Lammen, 12-Aug-2023)