We are using some terminology from logic.
Like "object", "truth value", "predicate", "quantifier",
"definition", "declaration", "primitive", "axiom", "theorem", "proof",
"and", "or", "if", "then", "foreach", "exists" ...

Any "thing" is an "object".
We show them by lowercase Greek letters: α β γ
When we say foreach(α), we mean for any object α

A "predicate" assigns a "truth value" to an "ordered tuple" of objects.
We use open face capital latin letters to show them: ℙ ℚ ℝ
ℙ(α) is interpreted as the object α has the "property" ℙ
ℝ(α,β) means the object α is in a "relation" ℝ with the oject β


Equals(α,β) or α=β is "defined" as
foreach(ℙ) ℙ(α) if and only if ℙ(β)

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" here, 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) ℙ(a) means foreach(α) if Element(α) then ℙ(α)
foreach(A) ℙ(A) means foreach(α) if Class(α)   then ℙ(α)

exists(a) ℙ(a) means exists(α) Element(α) and ℙ(α)
exists(A) ℙ(A) means exists(α) Class(α) and ℙ(α)

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