Confusion when applying the Empty Set to the Axiom Schema of Replacement In Kenneth Kunen's "The Foundations of Mathematics", one of the ZFC Axioms (The Axiom Schema of Replacement) reads as follows:
$$\forall A \Big ( \forall x \in A \  \exists !y \varphi(x,y) \rightarrow \exists B \ \forall x \in A \ \exists y \in B \ \varphi (x,y) \Big)$$
which can be reformulated more strictly as:
$$\forall A \Big ( \forall x \big(x\in A \rightarrow \exists!y \varphi(x,y)\big) \rightarrow \exists B \ \forall x \big(x \in A \rightarrow \exists y ( y \in B \land \varphi (x,y))\big)\Big)$$.
Consider when $A = \emptyset$, which has the property that $\forall x (x \notin \emptyset)$.
Looking at the more strict version of the axiom, we have:
$$\forall x \big(\color{red}{x\in \emptyset \rightarrow \exists!y \varphi(x,y)}\big) \rightarrow \exists B \ \forall x \big(x \in \emptyset \rightarrow \exists y ( y \in B \land \varphi (x,y))\big)$$
The "embedded" implication $\color{red}{x\in \emptyset \rightarrow \exists!y \varphi(x,y)}$ is vacuously true for any $x$. Therefore, the antecedent of the axiom when $A = \emptyset$ is true. Because we now have "access" to the consequent, this means that there exists a set of the following form:
$$\exists B \ \forall x \big(x \in \emptyset \rightarrow \exists y ( y \in B \land \varphi (x,y))\big)$$

Now, my question is, what exactly does $\exists B \ \forall x \big(x \in \emptyset \rightarrow \exists y ( y \in B \land \varphi (x,y))\big)$ mean?
Suppose $B'$ is a set that satisfies the formula: $\forall x \Big (x \in \emptyset \rightarrow \exists y \big (y \in B' \land \varphi(x,y) \big ) \Big )
$
Choose an arbitrary $x'$.
We know that $x' \in \emptyset \rightarrow \exists y \big ( y \in B' \land \varphi(x',y) \big )$ is a true statement.
However, because the antecedent of the implication is false, the truth of the implication can occur in two situations involving the consequent:

*

*$\exists y \big ( y \in B' \land \varphi(x',y) \big )$ is false


*$\exists y \big ( y \in B' \land \varphi(x',y) \big )$ is true
Situation 1. can be false in two (meaningfully) different ways:
1A. $\neg \exists y (y \in B')$. This would mean, by definition, that $B'$ is the empty set.
1B. $\neg \exists y \big (\varphi(x',y) \big )$ but $\exists y (y \in B')$. This would mean that $B'$ is not empty...but we cannot claim that any $y$ in the universe of all sets has a relationship with $x'$ as described by $\varphi$.
Situation 2. can be true in only one way:
2A. where $B'$ is non-empty and at least one $y$ has the property that $\varphi(x',y)$

Now, realize that the above comments were only made with respect to a particular $x$... (which we called $x'$)... in our domain of discourse (which is the universe of all sets). Obviously, because of the universal quantifier, claims will also be made for an x'', an x''', etc.
So, it seems as though the sets we can prove exist from this axiom when $A = \emptyset$ are the empty set and non-empty sets that may or may be related to an $x$ in the universe of all sets through $\varphi$.
Is this the correct interpretation?
If so, could some please help me understand what it means to prove the existence of a non-empty set that "may or may not" have particular properties? It's almost as if I am saying, "Here. I proved that an ambiguous object that I cannot describe with any clarity exists." I am having difficulties grasping what this means.
 A: 
what exactly does $\exists B \ \forall x \big(x \in \emptyset \rightarrow \exists y ( y \in B \land \varphi (x,y))\big)$ mean?

This formula means that there exists a set $B$ satisfying the condition $\forall x \big(x \in \emptyset \rightarrow \exists y ( y \in B \land \varphi (x,y))\big)$. Since for each set $x$, $ x \in \emptyset $  is false, the implication $x \in \emptyset \rightarrow \exists y ( y \in B \land \varphi (x,y))$ is true. So the condition is true (for each set $x$) and therefore the formula means that there exists (some) set $B$.
A: You are right: $(x \in \emptyset \to \exists ! x \varphi(x,y))$ being vacuously true, the Axiom holds also for $\emptyset$.
But what does the axiom means? It is a conditional that is universally quantified: thus, it is true for every set $A$.
When $A=\emptyset$ the antecedent of $(x \in A \to \exists ! x \varphi(x,y))$ is False and thus the formula is True.
Thus, we can apply Modus Ponens to derive the consequent of the axiom: $∃B  ∀x(x∈\emptyset → ∃y(y∈B ∧ φ(x,y)))$.
What does it mean this formula? It means that the universally quantified conditional: $∀x(x∈\emptyset → ∃y(y∈B ∧ φ(x,y)))$ holds for some set $B$.
But again: the antecedent $x ∈ \emptyset$ is False for every $x$.
Thus, formula $∀x(x∈\emptyset → ∃y(y∈B ∧ φ(x,y)))$ holds for an arbitraty set $B$.
Conclusion: the empty set is not a counter-example to the Axiom.

The annoying case $A=\emptyset$ may be easily avoided re-writing Kunen's Axiom (call it: $\text {KA}$) as follows:

$(\text {KA}_1) \ ∀A[A \ne \emptyset \to (∀x∈A ∃!yφ(x,y) → ∃B ∀x∈A ∃y∈B φ(x,y))]$

It is interesting to note that the two are equivalent:
(i) $\text {KA} \to \text {KA}_1$: easily done, using tautology: $P \to (Q \to P)$.
(ii) $\text {KA}_1 \to \text {KA}$.
We know that: $\lnot (x \in \emptyset)$. Thus, by tautology: $\lnot P \to (P \to Q)$ we have: $x \in \emptyset → (∃y \in B) \varphi(x,y)$.
By Generalization: $\exists B\forall x (x \in \emptyset → (∃y \in B) \varphi(x,y))$.
Finally: $∀x∈ \emptyset ∃!yφ(x,y) → \exists B\forall x (x \in \emptyset → (∃y \in B) \varphi(x,y))$, and thus, discharging the assumption $A=\emptyset$:

$A=\emptyset \to [∀x∈A ∃!yφ(x,y) → \exists B\forall x (x \in A → (∃y \in B) \varphi(x,y))].$

Now we apply Proof by Cases to the last formula and $\text {KA}_1$ to conclude with $\text {KA}$.

Comment: what troubles you in Kunen's formulation of the Axiom?
The gist of Replacement is to provide a new tool to manufacture "big" sets whose existence is not licensed by other axioms: pair, union, power-set, infinity, Specification schema.
The "procedure" provided by Replacement is quite simple: for every existing set $A$ and every "functional" formula $\varphi(x,y)$, as long as $x$ spans over $A$ we "collect" the values $y$ such that $\varphi(x,y)$ into a new set $B$.
What happens when $x$ spans over $\emptyset$? That no new set $B$ is produced, exactly because every existing $B$ satisfies the "procedure" described above.
Thus, again, the empty set is not a counter-example to Replacement. But to apply the axiom to it is simply pointless.


Having said that, a different formulation is more transparent:

$∀x∃!y \varphi(x,y) → ∀A∃B∀y[y∈B ↔ ∃x(x∈A ∧ \varphi(x,y))]$.

And different versions are equivalent.
