How to rigorously prove that if $A\times B\neq\emptyset$ then $(A\times B\subset X\times Y)\iff(A\subset X)\land (B\subset Y)$?

Question

I want to prove this formula as rigorous as possible. Here is my proof.

$\Rightarrow)$

We need to prove that $(A\not\subset X\lor B\not\subset Y)\land (A\times B\neq \emptyset)\Rightarrow A\times B\not\subset X\times Y$.

1. $A\not\subset X\land A\times B\neq\emptyset\Rightarrow\exists a\ a\in A\land a\notin X\ \land\ \exists s\ s\in A\times B \\ \Rightarrow a_0\in A\land a_0\notin X\land s_0\in A\times B\Rightarrow a_0\in A\land a_0\notin X\land\exists a\exists b\ a\in A\land b\in B\land s_0=(a,b) \\ \Rightarrow a_0\in A\land a_0\notin X\land a_1\in A\land b_1\in B\land s_0=(a_1,b_1)\\ \Rightarrow (a_0,b_1)\in A\times B\land (a_0,b_1)\notin X\times Y\Rightarrow\exists e\ e\in A\times B\land e\notin X\times Y\Rightarrow A\times B\not\subset X\times Y$

2. $B\not\subset Y\land A\times B\neq\emptyset\Rightarrow A\times B\not\subset X\times Y$

$\Leftarrow)$

$A\times B\not\subset X\times Y\Rightarrow \exists s\ s\in A\times B\land s\notin X\times Y \\ \Rightarrow s_0\in A\times B\land s_0\notin X\times Y\Rightarrow (\exists a\exists b\ a\in A \land b\in B\land s_0 = (a,b))\land s_0\notin X\times Y\\ \Rightarrow a_0\in A\land b_0\in B\land s_0 = (a_0,b_0)\land s_0\notin X\times Y \Rightarrow a_0\in A\land b_0\in B\land(a_0,b_0)\notin X\times Y\\ \Rightarrow a_0\in A\land b_0\in B\land (a_0\notin X \lor b_0\notin Y)\\ \Rightarrow (a_0\in A\land b_0\in B\land a_0\notin X)\lor(a_0\in A\land b_0\in B\land b_0\notin Y)\Rightarrow(\exists a\ a\in A\land a\notin X)\lor(\exists b\ b\in B\land b\notin Y)\\ \Rightarrow(A\not\subset X)\lor(B\not\subset Y)$

I'm pretty sure that, conceptually, this proof is correct. However, I might have accidentally skipped some steps, and, as for the others, I cannot fully justify them. So, can anyone correct this proof and provide its rigorous version?