Is this proof wrong?

Question

I am reading Decio Krause's quasi set theory (2010).

It allows ZF axiomatic set theory to exist within it but with a couple new fundamentals.

One of the theorems had a proof which I can't make sense of.

The following definitions and axioms are to understand the proof.

Definitions:
$Q(x)\iff x\text{ is a quasi-set (qset)}$
$D(x)\iff x\text{ is a classical thing}$
$Z(x)\iff x\text{ is a [ZF] set}$
$\forall_Qx$ is universal quantification relative to qsets
$\exists_Qx$ is existential quantification relative to qsets

Axiom 8: Qsets Whose Elements Are Classical Things Are Sets and Conversely $$\forall_Qx(\forall y(y\in x\implies D(y))\iff Z(x))$$

Axiom 10: The Empty Qset $$\exists_Qx\forall y(\neg(y\in x))$$ Let $x_{A10}:=\emptyset$

Theorem 7: The Empty Qset is a set

It is left as a theorem that the empty quasi set is a [ZF] set.

PROOF: (from the text)

"Since $y\in x$ is false by A10, then the antecedent of $\forall y(y\in x\implies D(y))$ is true, hence $Z(\emptyset)$ by A8"

CONFUSION

If $y\in x$ is false, and $y\in x$ is the antecedent, then how the antecedent be true?

Answer 1

Axiom A8 applied to $\emptyset$ is: $\forall y(y \in \emptyset \to D(y)) \leftrightarrow Z(\emptyset)$, from which:

$\forall y(y \in \emptyset \to D(y)) \to Z(\emptyset)$,

using Biconditional elimination rule.

From axiom A10 we have: $∀y(¬(y \in \emptyset))$ and thus:

1. $¬(y \in \emptyset)$ --- from A10 by UI

2. $¬(y \in \emptyset) \to [(y \in \emptyset) \to D(y)]$ --- using tautology $\lnot P \to (P \to Q))$

3. $(y \in \emptyset) \to D(y))$ --- from 1) and 2) by Modus Ponens

4. $\forall y ((y \in \emptyset) \to D(y))$ --- from 3) by UG

5. $Z(\emptyset)$ --- from A8 and 4) by Modus Ponens.