I'm doing the following transformations over a statement with an existential quantifier that I believe is valid, but I don't know how to justify it in my chain of equivalences:
$$ \begin{align} \exists y \in Y \{ y \in B \land &\exists x \in X \{ x \in A \} \} \\ &\iff \exists x \in X, y \in Y \{ x \in A \land y \in B \} \\ &\iff \exists x \in X \{ x \in A \land \exists y \in Y \{ y \in B \}\} \end{align} $$
I couldn't find an existing existential quantifier rule I could name here. Can this be justified, or am I missing something?
You should have access to a rule that when $z$ does not occur free in $P$ then $$(\exists z~Q(z))\wedge P \iff \exists z~(Q(z)\wedge P)$$
Do you have any trouble seeing why that is justified?
This also works in restricted domains, $(\exists z{\in}Z~Q(z))\wedge P\iff \exists z{\in}Z~(P\wedge Q(z))$
So applying this and the commutivity of conjunction, we have $$\begin{align} & \exists y{\in}Y~(y\in B\wedge (\exists x{\in}X~x\in A)) \\ \iff & (\exists y{\in}Y~y\in B)~\wedge~(\exists x{\in}X~x\in A) \\ \iff & (\exists x{\in}X~ x\in A)~\wedge~(\exists y{\in}Y~y\in B) \\ \iff & \exists x{\in} X~(x\in A\wedge (\exists y{\in}Y~y\in B)) \\[2ex] \iff & \exists x{\in}X~\exists y{\in} Y~(x\in A\wedge y\in B) \end{align}$$