My question is simple, as the title says: can I safely remove (or add) a quantifier if the variable bound to it is not used in any predicate following it?
As an example: I wanted to prove $$ \exists x(P(x) \implies \forall yP(y))$$ My proof went like this: $$ \exists x(P(x) \implies \forall yP(y)) \iff \exists x(\neg P(x) \lor \forall yP(y)) \iff \neg \forall xP(x) \lor \exists x \forall yP(y)$$ (The last equivalence follows from distributivity of existential quantifier over disjunction).
Now, we see that in the second clause the $x$ is not used, so it could be any element of the universe of discourse. Hence we remove it and replace the bound variable $y$ to $x$ to get: $$ \neg \forall xP(x) \lor \forall xP(x) $$ An obvious tautology. Q.E.D. (?)
It seems to me that all I've done is legal, at least assuming that the universe of discourse is not an empty set. Am I correct or can I not do this? Equivalently can I add quantifiers (like in the example below)? $$ \forall xP(x) \land Q(y) \iff \forall xP(x) \land \forall xQ(y) \iff \forall x(P(x) \land Q(y))$$