The author is defining the "set-builder" operator: $\{ x \mid \varphi(x) \}$ that "maps" a predicate (a formula $\varphi$ with free variable $x$) into a term (i.e. the "name" of an object).
It is well-known that the so-called unrestricted Comprehension Principle is inconsistent [see §1.3]: thus, not every predicate can meaningfully define a set.
The author uses the definitional schema illustrated at page 19 with the $x/y=z$ example.
Going back to Definition 11, the author illustrates it at page 34.
There are two possible cases:
(i) either there is a set $A$ such that $(\forall x)(x \in A \leftrightarrow \varphi(x))$,
in which case we define that the "set-builder" operator maps formula $\varphi$ to that set, or
(ii) there is no set $B$ such that $(\forall x)(x \in B \leftrightarrow \varphi(x))$,
in which case we "arbitrarily" define that the "set-builder" operator maps formula $\varphi$ to the empty set.
Maybe your confusion is due to the incorrect way of reading the definition:
"if $y$ is not an empty set, we don't go to the second element; if $y$ is indeed an empty set, then for any $x, x∈y$ is not true, which requires $\varphi(x)$ cannot be satisfied.
We are defining $y$, i.e. we have to start from the formula and "manufacture" the corresponding set.
Regarding:
I further found the second element confusing. Suppose indeed $\varphi(x)$ is not satisfiable,...
The issue is not the satisfiability of the formula; consider the discussion about Russell's paradox (page 6).
Into the formula $(\forall x) (x \in y \leftrightarrow \lnot (x \in x))$we are using $\lnot (x \in x)$ as $\varphi(x)$ and the formula is indeed satisfiable: $\lnot (\emptyset \in \emptyset)$.
Best Answer
The emptyset is the unique set $x$ satisfying the formula $\forall y(y\not\in x)$. "There is an emptyset" is natural-language shorthand for "$\exists x\forall y(y\not\in x)$."
If you prefer set-builder notation, then $\{y:y\not=y\}$ does the job: the condition "$y\not=y$" is not satisfied by any $y$s at all, and so $\{y:y\not=y\}=\emptyset$.
Note that we can't mix these approaches with abandon: the set-builder expression "$\{x: \forall y(y\not\in x)\}$" describes the set $\{\emptyset\}$, not $\emptyset$ itself! Also, note that despite its name set-builder notation is not guaranteed to build sets in general - for example, $\{x: x=x\}$ is a proper class (the "universal class"), as is $\{x: x\not\in x\}$ (the "Russell class").
Meanwhile, your proposal does not work since no set $x$ whatsoever (empty or not) has the property $\forall y(y\in x\leftrightarrow y\not\in x)$. The issue is that you've gotten the conclusion of your example argument strategy wrong: we don't conclude "$x\in X\iff x\not\in X$," merely "$x\in X\implies x\not\in X$" (which leaves "$x\not\in X$" as a stable option). That said, we can if we really want to combine your proposal with set-builder notation: since your proposed property does not in fact hold of any set, the set-builder notation $\{x: \forall y(y\in x\leftrightarrow y\not\in x)\}$ is yet another way of describing the emptyset.