Is this a valid way of using the axiom of replacement: A question arising when demonstrating that a set of Cartesian products exists The importance of this question recently came up during the construction of a set I needed for a proof required in an exercise in Tao's Analysis I book.
Restricting myself to axioms provided by Tao, I wanted to create a set of Cartesian products in following form:
$\Psi = \{ X \times D: D \in \Phi\}$ 
where $X$ is some arbitrary fixed set and $\Phi = \{D:D \subseteq Y\}$, where $Y$ is some arbitrary set. ($\Phi$ clearly exists because of the power set axiom and $X$ and $Y$ are sets that exist by assumption)
Now, the only way I could think of doing this is as follows:
Let $\Phi = \{A,B,C,...\}$
(From a previous exercise, I have already demonstrated that any cartesian product between two sets exists. Therefore, $X \times A$, $X \times B$, $X \times C$, ...are all sets that exists)
Now, Tao has previously "constructed" the set of natural numbers and, by the axiom of infinity, this set is infinite. If the number of elements in $\Phi$ is finite, you can define a set $I \subseteq \mathbb N$ such that the size of $I$ is $1 \leq n$ where $n$ is the finite size of $\Phi$.
However, consider the case where $\Phi$ contains infinitely many sets. In such a case, let $I = \mathbb N$. 
In either case, create the following bijective function:
$f:I \to \Phi$
$f: \text{ Arbitrary Assignment Rule }$ (e.g. $0 \mapsto A$, $1 \mapsto B$,...) 
Now, using the axiom of replacement:

$\{X \times D:  i \in I \land f(i) = D\}$

$\color{red}{\textrm{And this is where my question arises.}}$ I have never used the axiom of replacement like this. The form that I am exclusively familiar with reads as:
Given that $X$ exists, the set $\{y: x\in X \land f(x)=y\}$ exists. 
Comparing this to my highlighted statement, there are extra symbols present: the "$X \times$" in the symbology of $X \times D$ (i.e. it is not just "$D$"). 
Is this okay?
 A: The axiom of replacement requires a "(definable) class function", and it this case you have one: we have a "parameter" $X$ that is fixed and we can show for any set $D$ that $X \times D$ is a (uniquely determined) set in our axiom system (pairs axiom, powerset and comprehension, will prove that e.g.). So this "assignment" of $D$ to $X \times D$ (we could write $f_X(D)=X \times D$) is a "class function", not a function (which is a set) yet. 
But Axiom of Replacement to the rescue: if $\Phi$ is a set, then $\{f_X(D): D \in \Phi\} := \{y: \exists D \in \Phi: y=f_X(D)\}$ is a set, by an application of this axiom (which intuitively is OK, because we're just replacing all elements $D$ of $\Phi$ by their image under $f_X$, so we don't get "larger" sets this way and weird paradoxes will be avoided).
So $\{X \times D: D \in \Phi\}$ is indeed a valid set in full ZF (with replacement). This axiom was (IIRC) the addition of Fraenkel, and got his name attached to Zermelo's (who first came up with the formulation of most of the other axioms) as an homage. 
The extra $X$ is OK, it's a parameter (a free variable in the defining predicate) in the "class function", and this is explicitly allowed, the axiom is really an infintude of axioms, one for each class function (logical nitty gritty, as a class function is not a set, we cannot quantify over it). See Wikipedia for more details, or a good set theory book (Kunen, Jech, etc.)
