I am just starting self-studying Axiomatic Set Theory by Patrick Suppes. I have a doubt on the definition by abstraction.
Just to give some context, Suppes defines a set as
$y $ is a set $\leftrightarrow \exists x\in y\ \vee\ y=0$ (empty set)
I found the first element in Def 11's disjunction is enough. 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\in y$ is not true, which requires $\phi(x)$ cannot be satsified. Conversely, if $\phi(x)$ is not satisfiable, then $x\notin y$ for every $x$. Then, $y$ is an empty set. This already expresses out intuitive understanding.
I further found the second element confusing. Suppose indeed $\phi(x)$ is not satisfiable, in which case our intuition tells us $y=0$ (empty set). I can indeed find $B=0$ (empty set) too. $\forall x\ \neg \phi(x)$, and $\forall x\ \neg x\in B$. Thus, I conclude there exists $B=\phi$, $\forall x,x\in B\leftrightarrow \phi(x)$.
This contradicts the definition of Suppes. Am I wrong with the reasonings in both paragraphs above? Thanks.

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:
in which case we define that the "set-builder" operator maps formula $\varphi$ to that set, or
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:
We are defining $y$, i.e. we have to start from the formula and "manufacture" the corresponding set.
Regarding:
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)$.