Given the following predicate;
$(\exists x:X.P(x)\implies Q(x)) \wedge \forall y:X.P(y)$
Applying the distributive property of $\wedge$ / $\exists$
$\equiv \exists x:X.(P(x)\implies Q(x)) \wedge \forall y:X.P(y) $
Can you always 'move a universal quantifier under' an existential quantifier? (I'm not sure how to properly express this in English.)
What are the restrictions for applying this property?
Yes, that works!
The general principle is:
$\exists x \ \varphi(x) \land \psi \equiv \exists x (\varphi(x) \land \psi)$
where $\psi$ does not contain $x$ as a free variable.
And that applies here. The fact that in this case the $\psi$ contains a universal quantifier does not change this. In fact, even if you had $\forall x : X . P(x)$ on the right side it would still work, since it would still be true that $x$ is not a free variable in that formula.