Description: Move existential quantifier in and out of class substitution, with an explicit non-free variable condition. (Contributed by Giovanni Mascellani, 29-May-2019)