Everything is an object.
When we say foreach(α), we mean for any object α.
Here we are going to use some terminology from logic.
Like definition, declaration, primitive, predicate ...
Equals(α,β) or α=β is "defined" as
foreach(P) P(α) if and only if P(β)
equality is
reflective: foreach(α) α=α
symmetric: foreach(α,β) if α=β then β=α
transitive: foreach(α,β,γ) if α=β and β=γ then α=γ
Set Theory
starts here:
Belongs(α,β) or α∈β
This is a primitive/undefined "predicate".
First we "declare" two more predicates:
foreach(α,β) if (α∈β) then Element(α)
foreach(α,β) if (α∈β) then Class(β)
Then we "define" what is a set:
Set(α) == Element(α) and Class(α)
And what is not:
PureElement(α) == Element(α) but not Class(α)
PureClass(α) == Class(α) but not Element(α)
PureObject(α) == neither Element(α) nor Class(α)
Our "Pure Element" is what Euclid tried to "define" as a "Point".
You are welcome.
Case Convention
To achieve a concise and more readable notation for quantifiers,
a distinction is made between elements and classes based on letter case:
lowercase letters denote elements, while uppercase letters denote classes.
foreach(a) P(a) means foreach(α) if Element(α) then P(α)
foreach(A) P(A) means foreach(α) if Class(α) then P(α)
exists(a) P(a) means exists(α) Element(α) and P(α)
exists(A) P(A) means exists(α) Class(α) and P(α)
these conventions are fully compatible with quantifier negation "rules".
SubClasses
A⊆B means foreach(x) if x∈A then x∈B
This is a definition, based only on the yet totally undefined predicate ∈
Still we can prove that SubClass relation is both reflective and transitive:
foreach(A) A⊆A
foreach(A,B,C) if A⊆B and B⊆C then A⊆C
To show that the SubClass relation ∈ is an "order" relation among classes,
we must show that it is anti-symetric.
Using the defintion of equality, we can only prove half of it:
foreach(A,B) if A=B then A⊆B and B⊆A
But, we cannot prove the other side.
Why? Because there are "models" of a predicate ∈ which does not satisfy it!
We need to restrict its "declaration" using an "axiom".
Axiom of Extensionality
foreach(A,B) if A⊆B and B⊆A then A=B