a formula $\phi$ is said to be "precise" over theory $T$, denoted by $!^T(\phi)$ if $\exists x \forall y (y \in x \leftrightarrow \phi)$ is satisfied by a model of $T$, and if there cannot exist two models of $T$ such that $\exists x \forall y (y \in x \leftrightarrow \phi)$ is true in both models and one model proves $\exists y (y \in x \land \phi)$ and the other model proves $\not \exists y (y \in x \land \phi)$
Another more general definition:
a formula $\phi$ is said to be "very precise", denoted by $!!^T(\phi)$ over theory $T$ if $\exists x \forall y (y \in x \leftrightarrow \phi)$ is satisfied by a model of $T$ and if there is no formula $\psi$ such that there exists two models of $T$ such that $\exists x \forall y (y \in x \leftrightarrow \phi)$ is true in both models and one model proves $\exists y (y \in x \land \psi)$ and the other model proves $\not \exists y (y \in x \land \psi)$
Is the following theory denoted by $T$, and I'll name as "Precise Set Theory", properly defined? consistent? complete?
$T$ is the theory written in first order predicate logic with identity and membership, whose axioms are:
Define: $set(x) \equiv_{df} \exists y (x \in y)$
Extensionality: $\forall z (z \in x \leftrightarrow z \in y) \to x=y$
Class Comprehension: if $\phi$ is a formula in which $x$ doesn't occur, then all closures of $$\exists x \forall y (y \in x \leftrightarrow set(y) \land \phi)$$; are axioms.
Define: $x=\{y|\phi\} \equiv_{df} \forall y (y \in x \leftrightarrow \phi)$
Precision: $\forall \phi (!!^T(\phi) \to set(\{y| \phi\}))$
The idea is that sets are classes that are definable in a precise manner.