{(x,y)∈E^{2}  f(x) R f(y)}
For any family of a binary relations (R_{i})_{i∈I} on respective sets F_{i}, their product is the binary relation on P = ∏_{i∈I} F_{i} defined as{(x,y)∈P^{2}  ∀i∈I, x_{i} R_{i} y_{i}} = ⋂_{i∈I} π_{i}_{⋆}(R_{i}).
(It is actually in canonical bijection with the product of sets ∏_{i∈I} R_{i})Both operations can be combined in one step: for any family of functions f_{i} : E → F_{i}, the relation
{(x,y)∈E^{2}  ∀i∈I, f_{i}(x) R_{i} f_{i}(y)} = ⋂_{i∈I} f_{i}_{⋆}(R_{i})
is the preimage of the product relation of the R_{i} on P, by the function ⊓_{i∈I} f_{i} : E → P.These concepts will be later generalized to other firstorder structures.
A binary relation R on a set E will be said
reflexive ⇔  ∀x∈E, xRx ⇔ 𝛿_{E} ⊂ R ⇒ Dom R = Im R = E 
irreflexive ⇔  ∀x∈E, ¬(xRx) 
symmetric ⇔  (∀x,y∈E, xRy ⇒ yRx) ⇔ R ⊂ ^{t}R ⇔ R = ^{t}R ⇔ (R⃗) = (R⃖) 
antisymmetric ⇔  ∀x,y∈E, (xRy ∧ yRx) ⇒ x = y 
transitive ⇔  ∀x,y,z∈E, (xRy ∧ yRz) ⇒ xRz 
Example. Let A ⊂ E^{E} and R = ⋃_{f∈A} Gr f. Then
(Id_{E} ∈ A) ⇒  R is reflexive 
(∀f,g∈A, g⚬f ∈ A) ⇒  R is transitive 
(∀f∈A, f : E↔E ∧ f^{ 1}∈ A) ⇒  R is symmetric 
On the class of sets, the metarelation ⥬ (existence of a canonical bijection) is a metapreorder.
The Boolean pair V_{2} is naturally ordered by ⇒ which coincides
there with the usual order between numbers.
The resulting product order on V_{2}^{E} ⥬ ℘(E)
(and thus any set of sets) is that of inclusion (⊂).
{(x,y)∈E^{2}  R⃗(x) ⊂ R⃗(y)}.
Conversely, any preorder R on a set E is so definable from itself in both ways (exchanged by transposition):∀x,y∈E, R⃗(y) ⊂ R⃗(x) ⇔ x R y ⇔ R⃖(x) ⊂ R⃖(y)
Proof. Transitivity is equivalent to (∀x,y∈E, x R y ⇒ R⃗(y) ⊂ R⃗(x)) and to (∀x,y∈E, x R y ⇒ R⃖(x) ⊂ R⃖(y)).∀x∈E, (∀y∈E, R⃗(x) ⊂ R⃗(y) ⇒ y R x) ⇔ x R x ⇔ (∀y∈E, R⃖(x) ⊂ R⃖(y) ⇒ x R y). ∎
Thus R is the preimage of ⊂ by (R⃖). Moreover,∀x,y∈E, R⃖(x) = R⃖(y) ⇔ (R⃖(x) ⊂ R⃖(y) ∧ R⃖(y) ⊂ R⃖(x)) ⇔ (xRy ∧ yRx)
so that (R⃖) is injective if and only if R is an order.A strict order is a binary relation both transitive and irreflexive; and thus also antisymmetric.
Strict orders < bijectively correspond to orders ≤ byx < y
⇔ (x ≤ y ∧ x ≠ y).
x ≤ y ⇔
(x < y ∨ x = y).
∀x,y∈E, x < y
⇎ (y < x ∨ x = y)
∀x,y∈E, x = y ⇎
(y < x ∨ x < y)
∼_{f} = {(x,y)∈E 
f(x) = f(y)} = ∐(f_{•}⚬f)
Inj f ⇔ ∼_{f} = 𝛿_{E}
∀x,y∈E, x R y ⇔ R⃗(y) ⊂ R⃗(x) ⇔ R⃗(x) ⊂ R⃗(y) ⇔ R⃗(x) = R⃗(y)
Proof : ∀...∀f∈F^{E}, ∀h∈G^{E}, H = Im(f×h) ⇒
∼_{f} ⊂ ∼_{h} ⇔ (∀x,x'∈E,
f(x) = f(x′) ⇒
h(x) = h(x′)) ⇔ (∀(y,z),
(y′,z′) ∈ H, y=y′ ⇒ z=z′)
Dom H = Im f ∧
∀g∈G^{F}, h = g⚬f ⇔ H
⊂ Gr g. ∎
h/f = (Im f ∋y↦ ℩h[f_{•}(y)])
Gr (h/f) = Im (f×h)
Inj f ⇒ (f^{ 1} =
Id_{Dom f }/f ∧ h/f = h⚬f^{ 1})
∼_{f}
= ∼_{h} ⇔ Inj(h/f) ⇒ (h/f)^{1} = f/h
h = g⚬f ⇒ (∼_{f} ⊂ ∼_{h}
∧ h/f = g_{Im f})
⇒ (∼_{f} = ∼_{h}
⇒ f = (g_{Im f})^{−1}⚬h)
∀x,y ∈ Dom f, x ∼_{f} y ⇔ ∼⃗_{f}(x) = ∼⃗_{f}(y)
where (∼⃗_{f}) = f_{•}⚬f, reflects the injectivity of (f_{•}) which can be directly seen as
∀y∈Im f, ∀z, f_{•}(y) = f_{•}(z) ⇒ f_{•}(y) ∩ f_{•}(z) = f_{•}(y) ≠ ∅ ⇒ y = z.
(∀x,y∈E, x∈R⃗(y) ⇔ R⃗(x) = R⃗(y)) ⇔ (∀x∈E, ∀A∈P, x∈A ⇔ R⃗(x) = A) ⇔ Id_{P} = (R⃗_{E}_{•})
Thus if R is an equivalence relation then P is a partition.
Dom g = E ∧ (g_{•}) = Id_{P}
∴ P = Dom (g_{•})
= Im g
R = ∐g ⊂ E×E ∴ g
= R⃗_{E} ∴ (P
= R⃗[E] ∧ Id_{P} =
(R⃗_{E}_{•}))
∀x,y∈E, xRy ⇔ y∈ ℩{A∈P  x∈A} ⇔ (∃A∈P, x∈A ∧ y∈A) ⇔ (∀A∈P, x∈A ⇒ y∈A).
For any equivalence relation R on E, the partition R⃗[E] = Im (R⃗) is called the quotient of E by R, and written E/R, so that(R⃗) : E ↠ E/R.
For any x ∈ E, the set R⃗(x) = ℩{A∈E/R  x∈A} is called the class of x by R.f/R : E/R ↠ Im f
Inj f/R ⇔
R = ∼_{f}
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 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. Binary relations on a set ⇨ 2.10. Axiom of choice 
2.A. Time in set theory 2.B. Interpretation of classes 2.C. Concepts of truth in mathematics 

3. Algebra  4. Arithmetic  5. Secondorder foundations 