What is the justfication for splitting up statements and quantifiers?

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

• If you are writing or reading predicate logic proofs, how is it you haven't found out what proof rules, rule schemas & identities you are allowed to use/expect? (Rhetorical.) Mar 31, 2023 at 2:39
• You said "rhetorical", but I actually answered that question in the reply to Lee's answer below. Mar 31, 2023 at 9:14

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)$$