For each $(i, j) ∈ I × I$ let $C_{(i, j)} = A_i × B_j$, and let $P = I × I$ . Prove that $∪_{p∈P}C_p = (∪_{i∈I} A_i) × (∪_{i∈I} B_i)$. This is Velleman's exercise 4.1.11.b:
For each $(i, j) ∈ I × I$ let $C_{(i, j)} = A_i × B_j$, and let $P = I × I$ . Prove that $∪_{p∈P}C_p = (∪_{i∈I} A_i) × (∪_{i∈I} B_i)$.
My problem is with the proper translation of "$∪_{p∈P}C_p = (∪_{i∈I} A_i) × (∪_{i∈I} B_i)$". I believe the correct translation of the above statement is:
$∃(i,j) ∈ I^2((x,y) ∈ (A_i × B_j)) \iff ∃i ∈ I(x ∈A_i) \land ∃i ∈ I(y ∈B_i)$.
But I doubt it! Because if the above translation will be correct, then how one can use (instantiate) $y$ and $B_j$ to prove $y ∈ B_i$ for instance? 
Thanks.
 A: Fix $i'$ and $j'$, then for any $(a, b) \in C_{(i',j')}$ by definition $a\in \bigcup_{i\in I}A_i$ and $b\in \bigcup_{i\in I} B_i$, so $(a,b) \in \left(\bigcup_{i\in I}A_i\right) \times \left(\bigcup_{i\in I} B_i\right)$.
As this holds for any such $(a,b)$, we have
$$\bigcup_{(a,b) \in C_{(i',j')}}(a,b) = C_{(i',j')} \subseteq \left(\bigcup_{i\in I}A_i\right) \times \left(\bigcup_{i\in I} B_i\right)$$
As this holds for all $i', j'$
$$\bigcup_{(i',j') \in P} C_{(i',j')} \subseteq \left(\bigcup_{i\in I}A_i\right) \times \left(\bigcup_{i\in I} B_i\right)$$
Going the other way, for any $(a,b)\in \left(\bigcup_{i\in I}A_i\right) \times \left(\bigcup_{i\in I} B_i\right)$ then there exists at least one $i'$ and at least one $j'$ such that $a\in A_{i'}$ and $b\in B_{j'}$, so $(a,b) \in C_{(i', j')}$. As this holds for all $(a,b) \in \left(\bigcup_{i\in I}A_i\right) \times \left(\bigcup_{i\in I} B_i\right)$, so 
$$\left(\bigcup_{i\in I}A_i\right) \times \left(\bigcup_{i\in I} B_i\right) \subseteq \bigcup_{(i',j')\in P} C_{(i', j')}$$.
Equality follows from mutual inclusion.
A: I will write how you can do it your way. adfriedman’s answer goes another way, using the fact that equality of sets is equivalent to mutual inclusion. For all sets $D, D'$, $D=D'\iff\forall x(x\in D\iff x\in D')$. This may be a definition of equality of sets or a theorem. From where I am sitting, your translation seems correct. You forgot to bind $x$ and $y$ by universal quantifiers.
I do not understand how you want to instantiate $y$. The proof goes as follows.
$$\cup_{p∈P}C_p = (\cup_{i∈I}A_i) \times (\cup_{i∈I}B_i)$$
is equivalent to
$$\forall (x, y)((x, y)\in\cup_{p∈P}C_p \iff (x, y)\in(\cup_{i∈I}A_i) \times (\cup_{i∈I}B_i))$$
which is equivalent by definition of $C$ and a set union to
$$\forall (x, y)(\exists(i, j)\in I\times I((x, y)\in A_i\times B_j) \iff (x, y)\in(\cup_{i∈I}A_i) \times (\cup_{i∈I}B_i))$$
which is equivalent by definition of a Cartesian product of sets and a set union to
$$\forall (x, y)(\exists(i, j)\in I\times I(x\in A_i\land y\in B_j) \iff \exists i\in I(x\in A_i) \land \exists i\in I(y\in B_i)).$$
$x$ and $y$ are given. Prove the equivalence inside.
