Other kinds of metaobjects beyond the normal roles of elements,
sets and functions, will form new notions : those of operation, relation and tuple
will be formalized in 2.3. The new symbols they need are both definers (converting
metaobjects into the new objects) and evaluators (interpreting these objects
back to their roles as metaobjects).
But, like for unary relations (1.8), these new notions with their rolegiving symbols,
need not be primitive, as they can be naturally constructed as (represented by)
classes of existing objects (sets or functions), which can offer their tools (expressible features)
to the new objects. So, these extensions of set theory can be obtained by giving
definitions of their definer and evaluator symbols.
As the notions of operation and relation can be represented in several useful ways
by classes of old objects, which do not represent each new object by the same old
object (2.3), functors will be used for translations between the classes playing the
roles of these notions in the different ways (2.6, 2.8).
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.∀A, (∀x, C(x) ⇒ A(x)) ⇔ (Qx, A(x))
is proven by secondorder universal introduction (*) under a given condition on parameters, then C is a set that can be named by a new 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).
(*) we shall focus on cases whose proofs do not use any axiom obtained from a second order axiom by using A in the definition of its variable structure, though I am not sure if any such use is possible.
(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))).
Our first and main use cases of this principle are listed in the following table.
To justify all of these, (1) comes by finding C to be the formula so defined
from Q, while (3) is ensured by the absence of any "negative" occurrence
of A in Q (inside a negation, an equivalence, or left of a ⇒).
This leaves (2) as the easy remaining condition to check.
The first column recalls the above generic abbreviations ; each other
column gives an effective example. The K line gives the notations for the
set theoretical symbols so introduced.
K  {y∈E  B(y)}  ⋃E  Im f  ∅  {y}  {y,z} 
C(x)  x∈E ∧ B(x)  ∃y∈E, x∈ y  ∃y∈Dom f, f(y)=x  0 
x=y  x=y ∨ x=z 
dK  ∀x∈E, dB(x)  Set(E)∧∀y∈E, Set(y) 
Fnc(f)  1 
1 
1 
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) 
The value of the setbuilder K={x∈E  B(x)} first defined in 1.8
as a class, thus with an open quantifier (∀x, x∈K ⇔
Set(K) ∧ (∀x∈K, x∈E ∧ B(x)) ∧ (∀x∈E, B(x) ⇒ x ∈ K)
or more shortly Set(K) ∧ K ⊂ E ∧ (∀x∈E, x ∈ K ⇔ B(x)). Like the axioms for functions, this is an axiom schema by secondorder universal elimination on ∀B, so with all unary predicates B defined by bounded formulas with parameters.The 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.(f : E → F) ⇔ (Fnc(f) ∧ Dom f = E ∧ Im f ⊂ F)
A set F such that Im f ⊂ F (i.e. ∀x ∈ Dom f, f(x) ∈ F), is called a target set of f. The empty set ∅ is the only set without element, and is
included in any set (∀_{Set}E, ∅ ⊂ E).
Thus, (E=∅ ⇔ E ⊂ ∅ ⇔ ∀x∈E, 0), and
thus (E ≠ ∅ ⇔ ∃x∈E, 1).
The presence of this constant symbol ∅ ensures the existence of a set; for any set
E we also get ∅ = {x∈E  0}. We have ⋃∅ =∅.
As (Dom f = ∅ ⇔ Im f = ∅) and (Dom f = Dom g = ∅
⇒ f = g), the only function with domain ∅ is called the empty function ∅_{↦}.
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.
(∃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 and y we have {x, y} = {y, x}. If x ≠ y, the set {x, y} with 2 elements x and y is called a pair.
For any set E, the identity function on E is defined byId_{E} = (E ∋ x ↦ x).
Thus,
Dom Id_{E} = E = Im Id_{E}
∀x∈E, Id_{E}(x) = x.
Set theory and Foundations of Mathematics  
1. First foundations of mathematics  
2. Set theory  
2.1.
First axioms of set theory ⇦ 2.2. Set generation principle ⇨ 2.3. Tuples 2.4. Uniqueness quantifiers 2.5. Families, Boolean operators on sets 2.6. Graphs 2.7. Products and powerset 
2.8. Injections, bijections 2.9. Properties of binary relations 2.10. Axiom of choice 
Time
in set theory Interpretation of classes Concepts of truth in mathematics 

3. Algebra  4. Arithmetic  5. Secondorder foundations 