To explain the title, in proving $X \times Y = \emptyset \iff X = \emptyset \vee Y = \emptyset$, we have the following
\begin{align*} X \times Y = \emptyset &\iff \forall x \forall y \left((x,y) \notin X \times Y\right)\\ &\iff \forall x \forall y \left(x \notin X \vee y \notin Y\right) \\ &\iff \forall x (x \notin X) \vee \forall y (y \notin Y) \\ &\iff X = \emptyset \vee Y = \emptyset , \end{align*}
and in particular going from the second to the third line, we can (?) split up the statement $(x \notin X \vee y \notin Y)$ and quantifiers $\forall x \forall y$ into two separate statements each with its own quantifier. I'm not sure why this is true. It seems obvious that this is true, but is there a proof, or is it axiomatic? Or is it not true at all?
Thanks in advance - recently deleted a completely wrong proof of this statement so hopefully this one is at least correct
You could insert the following intermediate steps: \begin{align*} \forall x \forall y \left(x \notin X \vee y \notin Y\right) & \iff \forall x\bigl( \forall y (x \notin X \vee y \notin Y) \bigr) \\ & \iff \forall x\bigl(x \notin X \vee \forall y (y \notin Y)\bigr) \\ & \iff \bigl(\forall x (x \notin X)\bigr) \vee \bigl(\forall y (y \notin Y) \bigr) \end{align*} The second and third steps are applications of one of the Laws of Quantifier Movement in predicate logic, which says that if the free variable $x$ does not occur in the statement $P$ then you can move a universal $x$ quantifier into an "or" statement that involves $P$, in the following manner: $$\forall x (P \vee Q(x)) \iff P \vee (\forall x Q(x)) $$ I think of this as an "infinite" version of de Moivre's Theorem: if $x_1,x_2,...$ is a "list" of the values of $x$ then $$(P \vee Q(x_1)) \wedge (P \vee Q(x_2)) \wedge \cdots \iff P \vee (Q(x_1) \wedge Q(x_2) \wedge \cdots) $$