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))$$
Yes, this is correct. More precisely, if $P$ is any formula in which the variable $x$ does not appear, then $\exists x P$ and $\forall x P$ are each equivalent to $P$ over any nonempty universe of discourse (if you don't know the universe is nonempty, all you can say is $\exists x P \implies P$ and $P\implies\forall x P$).
(To be clear, if you're working in some specific formal deductive system rather than the informal logic that mathematicians usually work with, you would need to justify these statements using only the rules of your deductive system. Exactly how you do this depends on what your deductive system is.)