The article you referred to is the second of the two axiomatic articles of the Mizar Mathematical Library. As described on that site:
All other texts undergo verification by Mizar to be correct consequences of those axioms. The Mizar system assists the author of a new text in preparing available terminology and results, verifies the claims of the text and extracts facts and definitions for inclusion into the library.
So the article you referred to (TARSKI) (note that the version you read was human written abstract + latexed version of the human written article for the Mizar system, the latter being able to be understood by the machine) was explicitly written as foundation for a strict computational verification system. As such, you can't simply be
Using the definition of a set as a "class that is a member of a class"
because that is not what it is built on. The axiomatics, as well as Mizar in general, are covered in "Mizar in a Nutshell" by Adam Grabowski et al.
The other one of the two axiomatic articles is literally HIDDEN. The important logical concepts (e.g. $\land$
not (for predicates) or
non (for attributes), $\Rightarrow$
ex) are wired directly into the software and grammar of the Mizar language, but explicit modes (what kind of something else something can be, like an
object or a
set) or explicit predicates (saying that one or several something(s) are in some relation to another or not, like $x=y$
x = y, $x\neq y$
x <> y and $x\in X$
x in X) which basically the foundation to be even able to talk about axioms haven't been declared implicitly in the software, but explicitly in HIDDEN. They just are. And based on that, the axioms in TARSKI could be defined from the programming point of view. Or as it is put in "Mizar in a Nutshell":
[HIDDEN] documents a part of the Mizar axiomatics – it
shows how the primitives of set theory are introduced in the Mizar Mathematical
"Mizar in a Nutshell" goes through each of the short axiomatic articles. It states
[TARSKI] defines axiomatic foundations of the Tarski-
Grothendieck set theory: extensionality axiom [TARSKI:2] [...]
and goes on with the rest of the article, thereby implicitly stating that TARSKI:1 ("everything is a set") is not directly part of the TG axioms, but simply a part of the Mizar axiomatics. In fact, one could have left objects out of the whole axiomatization and sometimes I wonder if that wouldn't have been better, or just introduce "object" as a different notation of set, but in the end, it basically amounts to the same thing, but improves readability alot, depending on an author wanting to emphasize if a certain "thing" is an
object or rather a
set (which e.g. can be
empty or stand on the right side of an
If you are interested in it, the empty set is derived from these axioms here.