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  
2. Set theory  
2.1.
Formalization of set theory ⇦ 2.2. Set generation principle ⇨ 2.3. Tuples, families 2.4. Boolean operators on sets 2.5. Products, graphs and composition 2.6. Uniqueness quantifiers, functional graphs 2.7. The powerset 2.8. Injectivity and inversion 
2.9. Binary relations ; order 2.10. Canonical bijections 2.11. Equivalence relations, partitions 2.12. Axiom of choice 2.13. Galois connection 
Time
in set theory Interpretation of classes Concepts of truth in mathematics 

3. Algebra  4. Arithmetic  5. Secondorder foundations 