∀x, ∀_{Fnc} x, 
¬(Set(x) ∧ Fnc(x)) Set(Dom x) 
∀E,
∀(parameters), ∀_{Set}E, ∀_{Set}F, 
Fnc(E ∋ x ↦ t(x)) for any term t E ⊂ F ⊂ E ⇒ E=F (Axiom of Extensionality). 
(∀x ∈ F, R(x)) ⇔ (∀x ∈ E, R(x))
and similarly for ∃.Axioms for functions. The following axioms relate function definers with function evaluators for any functor t (to be replaced by all terms that can define it; the first of these axioms suffices to sum up the other 3) : for all values of parameters of t, any set E included in the definiteness class of t (this condition ∀x∈E, dt(x) is the definiteness condition for (E ∋ x ↦ t(x))), and all functions f and g,
f = (E ∋ x ↦ t(x))
⇔ ( Dom f = E ∧ (∀x∈E, f(x)
= t(x)))
Dom (E ∋ x ↦ t(x)) = E
∀x ∈ E, (E ∋ y ↦ t(y))
(x) = t(x)
(Dom f = Dom g ∧ ∀x∈Dom f, f(x)
= g(x)) ⇒ f = g
Metaobjects behaving as objects with another role beyond sets and functions, will be represented as another kind of objects (operations, relations, tuples), and the conversion tools from roles (metaobjects) to objects will be completed by new conversion tools from objects into their roles. But this can be done inside the same set theory (just by developing it), as already present objects (sets or functions) can be found to naturally play the roles of these new objects. So, the new notions can be defined as classes of existing objects (that will offer their expressible features to the new objects), while the tools of interpretation and definition of objets (converting objects into their roles of metaobjects and inversely) are defined as abbreviations of some fixed expressions. Then, the only needed functors of conversion between objects playing the role of the same metaobject by different methods (expressions), will relate the different objects of old kinds that usefully represent in different ways the same object of the new kind.
f ≈ (E ∋ x ↦
(F ∋ y ↦ t(x,y))) = g
f(x,y) = g(x)(y) = t(x,y)
The formalization of nary relations involves an (n+1)ary predicate of evaluation, and a definer binding n variables on a formula. We may either see nary relations as particular cases of nary operations (representing Booleans as objects), or see nary operations as particular cases of (n+1)ary relations (see 2.3). And just like operations, relations can be reduced to the unary case in 2 ways : by currying (with n−1 uses of the function definer and 1 use of the setbuilder, as will be done in 2.3 with n=2), or using tuples (2.1).
Set theory and Foundations of Mathematics  
1. First
foundations of mathematics 1.1. Introduction
to the foundations of mathematics
1.2. Variables, sets, functions and operations 1.3. Form of theories: notions, objects, metaobjects 1.4. Formalizing types and structures 1.5. Expressions and definable structures 1.6. Connectives 1.7. Classes in set theory 1.8. Binders in set theory 1.9. Quantifiers ⇦ 
1.10. Formalization of set theory 
Philosophical
aspects
⇨ Time
in set theory ⇨ Interpretation of classes 

2. Set theory (continued)  3. Model theory 