x ∈ E ⇔ (∃y∈E, x = y)
but is not generally definable from it in return by any bounded formula, as its definition involves an open quantifier.Philosophically speaking, the perception of a set as a class (ability to classify each object as belonging to it or not) does not suffice to provide its full perception as a set, that is the perspective over all its elements as coexisting. The above formula can be seen as confirming this view of a set as a coexistence of its elements, by describing the property of belonging to a set as a form of existence with respect to this set. Thus, Russell's paradox can be read as saying that mathematical objects cannot all coexist as a completed totality. The explanation of 1.7 that no set theoretical universe can be the ultimate one is just another aspect of this, as will be further commented in philosophical pages.
Set generation principle. For any class C defined by a bounded formula, if ∀_{C} is found equivalent to the quantifier Q defined by another bounded formula (whose free variables are the parameters of C and a variable unary predicate symbol A), by formally proving by secondorder universal introduction (under a given condition on parameters) that∀A, (∀x,C(x) ⇒ A(x)) ⇔ (Qx, A(x))
then C is a set that can be named by an operator symbol K added to the language of set theory, with these parameters as arguments, and the following axiom which expresses K = C by double inclusion: For all values of parameters satisfying the condition,Set(K) ∧ (∀x∈K, C(x)) ∧ (Qx, x ∈ K).
(The involved secondorder universal introduction can accept a proof using an already accepted axiom schema applied to an expression using A, thus beyond the strict concept of provability in the firstorder version of set theory ; I am not sure if this is ever used or not)
(1) ∀x, (C(x) ⇔ Q*y, x=y)
(in fact we just need ∀x, C(x) ⇒ Q*y,
x=y)
(2) Qx, C(x)
(3) ∀A, ∀B, (∀x, A(x) ⇒ B(x))
⇒ ((Qx, A(x)) ⇒ (Qx, B(x))).
The first column recalls the above generic abbreviations while each other column gives an effective example of expressions on which it works. The K line gives the notations for the set theoretical symbols so introduced.
dK  ∀x∈E, dB(x)  Set(E)∧∀x∈E, Set(x) 
Fnc(f)  1 
1 
1 
C(x)  x∈E ∧ B(x)  ∃y∈E, x∈ y  ∃y∈Dom f, f(y)=x  0 
x=y  x=y ∨ x=z 
Qx, A(x)  ∀x∈E, B(x)⇒A(x)  ∀y∈E, ∀x∈y, A(x)  ∀x∈Dom f, A(f(x))  1  A(y)  A(y) ∧ A(z) 
Q*x,A(x)  ∃x∈E, B(x) ∧ A(x)  ∃y∈E, ∃x∈y, A(x)  ∃x∈Dom f, A(f(x))  0 
A(y)  A(y) ∨ A(z) 
K  {y∈E  B(y)}  ⋃E  Im f  ∅  {y}  {y,z} 
Set(K) ∧ (∀x∈K, x∈E ∧ B(x)) ∧ (∀x∈E, B(x) ⇒ x ∈ K)
or more shortlySet(K) ∧ K ⊂ E ∧ (∀x∈E, x ∈ K ⇔ B(x))
with which the proof of Russell's paradox would be writtenThe functor ⋃ is the union symbol, and its axioms form the axiom of union.
The set Im f of values of f(x) when x ranges over Dom f, is called the image of f. The empty set ∅ is the only set without element, and is
included in any set E (∅ ⊂ E).
Thus, (E=∅ ⇔ E ⊂ ∅ ⇔ ∀x∈E, 0), and
thus (E ≠ ∅ ⇔ ∃x∈E,1).
This constant symbol ∅ ensures the existence of a set; for any set
E we also get ∅ = {x∈E  0}.
That a variable may have empty range, is no obstacle for fixing it. In particular,
developing an inconsistent theory means studying a fixed system whose range
of possibilities is empty. We may actually need to do so in order to discover a
contradiction there, which means to prove that no such system exists.
As (Dom f = ∅ ⇔ Im f = ∅) and
(Dom f = Dom g = ∅ ⇒ f = g), the only
function with domain ∅ is called the empty function.
(∃x∈E, A(x)) ⇔ {x∈E  A(x)} ≠ ∅ ⇔ (1 ∈ Im(E∋x ↦ A(x))).
For all x, {x,x} = {x}. Such a set with only one element is called a singleton.For all x, y, {x, y} = {y, x}. If x ≠ y, the set {x, y} with 2 elements x and y is called a pair.
Set theory and
Foundations of mathematics 

1. First
foundations of mathematics 
⇨ Philosophical
aspects 
1.1. Introduction
to the foundations of mathematics 1.2. Variables, sets, functions and operations 
Intuitive representation and
abstraction
Platonism vs Formalism 
1.3. Form of theories: notions, objects, metaobjects 
Realistic vs. axiomatic theories

1.4. Formalizing types and structures 1.5. Expressions and definable structures 
Time
in Model theory
The time of interpretation
The metaphor of the usual time The finite time between expressions 
1.6. Connectives 1.7. Classes in set theory 
The infinite time between theories
Zeno's Paradox 
1.8. Binders in set theory  Time
in Set theory
Expansion of the set
theoretical universe
Can a set contain itself ? 
1.9. Quantifiers 
The relative sense of open
quantifiers
Interpretation
of classesClasses in an expanding
universe
Concrete examples 
1.10. Formalization of set theory ⇦ 1.11. Set generation principle 
⇨ Justifying the set
generation principle Concepts of truth in mathematics Alternative logical
frameworks

⇨ 2. Set theory (continued)  3. Algebra  4. Arithmetic  5. Secondorder foundations 