avewright/proofwiki-math huggingface dataset:
Theorem: Equivalent Characterizations of Abelian Group

Let $G$ be a group.
{{TFAE}}
{{begin-axiom}}
{{axiom | n = 1
        | t = $G$ is abelian
}}
{{axiom | n = 2
        | t = $\forall a, b \in G: \paren {a b}^{-1} = a^{-1} b^{-1}$
}}
{{axiom | n = 3
        | t = {{Defof|Cross Cancellation Property}}: $\forall a, b, c \in G: a b = c a \implies b = c$
}}
{{axiom | n = 4
        | t = {{Defof|Middle Cancellation Property}}: $\forall a, b, c, d, x \in G: a x b = c x d \implies a b = c d$ 
}}
{{axiom | n = 5
        | t = the opposite group to $G$ is $G$ itself.
}}
{{end-axiom}}

Proof:
=== $(1)$ iff $(2)$ ===
See Inversion Mapping is Automorphism iff Group is Abelian.
{{qed|lemma}}
{{explain|There's a better link that proves this one, but IIRC it's difficult to find. I've been tidying up this recently, I'll see if I can find it in a bit.}}
Theorem: Relation Symmetry

Every non-null relation has exactly one of these properties: it is either:
:symmetric,
:asymmetric or
:non-symmetric.

Proof:
Let $\RR \subseteq S \times T$ denote an arbitrary relation on $S \times T$, for $S$ and $T$ arbitrary sets.
First we deal with the case where $\RR = \O$.
From Relation both Symmetric and Asymmetric is Null, the null relation ''is'' both symmetric and asymmetric.
So, let us assume that $\RR \ne \O$.
Let $\RR$ be symmetric.
Then $\RR$ is not asymmetric by definition.
Also, $\RR$ is not non-symmetric by definition.
Let $\RR$ be asymmetric.
Then $\RR$ is not symmetric by definition.
Also, $\RR$ is not non-symmetric by definition.
If $\RR$ is not symmetric, and $\RR$ is not asymmetric, then $\RR$ is non-symmetric by definition.
{{qed}}
Theorem: Asymmetric Relation is Antisymmetric

Let $\RR$ be an asymmetric relation.
Then $\RR$ is also antisymmetric.

Proof:
Let $\RR$ be asymmetric.
Then from the definition of asymmetric:
:$\tuple {x, y} \in \RR \implies \tuple {y, x} \notin \RR$
Thus:
:$\neg \exists \tuple {x, y} \in \RR: \tuple {y, x} \in \RR$
Thus:
:$\set {\tuple {x, y} \in \RR \land \tuple {y, x} \in \RR} = \O$
Thus:
:$\tuple {x, y} \in \RR \land \tuple {y, x} \in \RR \implies x = y$
is vacuously true.
{{qed}}
Theorem: Asymmetric Relation is Antireflexive

Let $S$ be a set.
Let $\RR \subseteq S \times S$ be a relation on $S$.
Let $\RR$ be asymmetric.
Then $\RR$ is also antireflexive.

Proof:
Let $\RR$ be asymmetric.
Then, by definition:
:$\tuple {x, y} \in \RR \implies \tuple {y, x} \notin \RR$
{{AimForCont}} $\tuple {x, x} \in \RR$.
Then:
{{begin-eqn}}
{{eqn | l = \tuple {x, x} \in \RR
      | o = \implies
      | r = \tuple {x, x} \notin \RR
      | c = {{Defof|Asymmetric Relation}}
}}
{{eqn | ll= \leadsto
      | l = \tuple {x, x} \notin \RR
      | o =
      | c = Proof by Contradiction
}}
{{end-eqn}}
Thus $\RR$ is antireflexive.
{{qed}}
Theorem: Antireflexive and Transitive Relation is Asymmetric

Let $\RR \subseteq S \times S$ be a relation which is not null.
Let $\RR$ be antireflexive and transitive.
Then $\RR$ is also asymmetric.

Proof:
Let $\RR \subseteq S \times S$ be antireflexive and transitive.
That is:
{{begin-eqn}}
{{eqn | l = \forall x \in S: 
      | o = 
      | r = \tuple {x, x} \notin \RR
      | c = {{Defof|Antireflexive Relation}}
}}
{{eqn | l = \tuple {x, y} \in \RR \land \tuple {y, z} \in \RR
      | o = \implies
      | r = \tuple {x, z} \in \RR
      | c = {{Defof|Transitive Relation}}
}}
{{end-eqn}}
We have that $\RR$ is not null.
{{AimForCont}} $\RR$ is not asymmetric.
So, by definition, $\exists \tuple {x, y} \in \RR: \tuple {y, x} \in \RR$.
Then from the transitivity of $\RR$ that would mean $\tuple {x, x} \in \RR$.
But that would contradict the antireflexivity of $\RR$.
Therefore:
:$\tuple {x, y} \in \RR \implies \tuple {y, x} \notin \RR$
and $\RR$ has been shown to be asymmetric.
{{qed}}
Theorem: Antitransitive Relation is Antireflexive

Let $S$ be a set.
Let $\RR \subseteq S \times S$ be a relation on $S$.
Let $\RR$ be antitransitive.
Then $\RR$ is also antireflexive.

Proof:
Suppose $\RR \subseteq S \times S$ is not antireflexive.
Then $\exists x \in S: \tuple {x, x} \in \RR$. (In the case of $\RR$ being reflexive, the property holds for ''all'' $x \in S$.)
Thus $\RR$ is not antitransitive:
{{begin-eqn}}
{{eqn | o =
      | r = \tuple {x, x} \in \RR \land \tuple {x, x} \in \RR
      | c =
}}
{{eqn | o = \leadsto
      | r = \tuple {x, x} \in \RR
      | c = Rule of Idempotence
}}
{{end-eqn}}
... which means $\exists x \in S$ such that the condition for antitransitivity is broken.
So $\RR \subseteq S \times S$ has to be antireflexive.
{{Qed}}
Theorem: Symmetric Transitive and Serial Relation is Reflexive

Let $\RR$ be a relation which is:
:symmetric
:transitive
:serial.
Then $\RR$ is reflexive.
Thus such a relation is an equivalence.

Proof:
Let $S$ be a set on which $\RR$ is a relation which is symmetric, transitive and  serial.
As $\RR$ is symmetric:
:$x \mathrel \RR y \implies y \mathrel \RR x$
As $\RR$ is transitive:
:$x \mathrel \RR y \land y \mathrel \RR x \implies x \mathrel \RR x$
As $\RR$ is serial:
:$\forall x \in S: \exists y \in S: x \mathrel \RR y$
Let $x \in S$.
Then
{{begin-eqn}}
{{eqn | q = \exists y \in S
      | l = \tuple {x, y}
      | o = \in
      | r = \RR
      | c = as $\RR$ is serial
}}
{{eqn | ll= \leadsto
      | l = \tuple {y, x}
      | o = \in
      | r = \RR
      | c = as $\RR$ is symmetric
}}
{{eqn | ll= \leadsto
      | l = \tuple {x, x}
      | o = \in
      | r = \RR
      | c = as $\RR$ is transitive
}}
{{end-eqn}}
Thus:
:$\forall x: x \mathrel \RR x$
and by definition $\RR$ is reflexive.
It follows by definition that such a relation is an equivalence relation.
{{qed}}
Theorem: Inverse Relation Properties

Let $\RR$ be a relation on a set $S$.
If $\RR$ has any of the properties:
:Reflexive
:Antireflexive
:Non-reflexive
:Symmetric
:Asymmetric
:Antisymmetric
:Non-symmetric
:Transitive
:Antitransitive
:Non-transitive
then its inverse $\RR^{-1}$ has the same properties.

Proof:
=== Reflexivity ===
{{:Inverse of Reflexive Relation is Reflexive}}
Theorem: Properties of Restriction of Relation

Let $S$ be a set.
Let $\RR \subseteq S \times S$ be a relation on $S$.
Let $T \subseteq S$ be a subset of $S$.
Let $\RR {\restriction_T} \subseteq T \times T$ be the restriction of $\RR$ to $T$.
If $\RR$ on $S$ has any of the properties:
* Reflexive
* Antireflexive
* Symmetric
* Antisymmetric
* Asymmetric
* Transitive
* Antitransitive
* Connected
... then $\RR {\restriction_T}$ on $T$ has the same properties.

Proof:
=== Reflexivity ===
Theorem: Relation is Antireflexive iff Disjoint from Diagonal Relation

Let $\RR \subseteq S \times S$ be a relation on a set $S$.
Then:
:$\RR$ is antireflexive
{{iff}}
:$\Delta_S \cap \RR = \O$
where $\Delta_S$ is the diagonal relation.

Proof:
=== Necessary Condition ===
Let $\RR$ be an antireflexive relation.
Let $\tuple {x, y} \in \Delta_S \cap \RR$.
By definition:
:$\tuple {x, y} \in \Delta_S \implies x = y$
Likewise, by definition:
:$\tuple {x, y} \in \RR \implies x \ne y$.
Thus:
:$\Delta_S \cap \RR = \set {\tuple {x, y}: x = y \land x \ne y}$
and so:
:$\Delta_S \cap \RR = \O$
{{qed|lemma}}
Theorem: Inverse Relation Equal iff Subset

Let $S$ and $T$ be sets. Let $\RR \subseteq S \times T$ be a relation.
If $\RR$ is a subset or superset of its inverse, then it equals its inverse.
That is, the following are equivalent:
{{begin-eqn}}
{{eqn | n = 1
      | l = \RR
      | o = \subseteq
      | r = \RR^{-1}
}}
{{eqn | n = 2
      | l = \RR^{-1}
      | o = \subseteq
      | r = \RR
}}
{{eqn | n = 3
      | l = \RR
      | r = \RR^{-1}
}}
{{end-eqn}}

Proof:
=== $(1)$ implies $(2)$ ===
Suppose $\RR \subseteq \RR^{-1}$.
Then:
{{begin-eqn}}
{{eqn | l = \tuple {a, b}
      | o = \in
      | r = \RR^{-1}
      | c =
}}
{{eqn | ll= \leadsto
      | l = \tuple {b, a}
      | o = \in
      | r = \RR
      | c = {{Defof|Inverse Relation}}
}}
{{eqn | ll= \leadsto
      | l = \tuple {b, a}
      | o = \in
      | r = \RR^{-1}
      | c = {{Defof|Subset}} (as $\RR \subseteq \RR^{-1}$)
}}
{{eqn | ll= \leadsto
      | l = \tuple {a, b}
      | o = \in
      | r = \RR
      | c = {{Defof|Inverse Relation}}
}}
{{end-eqn}}
Hence $\RR^{-1} \subseteq \RR$.
{{qed|lemma}}
Theorem: Relation is Symmetric iff Inverse is Symmetric

A relation $\RR$ is symmetric {{iff}} its inverse $\RR^{-1}$ is also symmetric.

Proof:
Let $\RR$ be symmetric.
Then from Relation equals Inverse iff Symmetric:
:$\RR = \RR^{-1}$
The result follows.
{{qed}}
Theorem: Composition of Relation with Inverse is Symmetric

Let $\RR \subseteq S \times T$ be a relation.
Then the composition of $\RR$ with its inverse $\RR^{-1}$ is symmetric:
:$(1): \quad \RR^{-1} \circ \RR$ is a symmetric relation on $S$
:$(2): \quad \RR \circ \RR^{-1}$ is a symmetric relation on $T$.

Proof:
{{Rewrite|In light of the more relaxed definition of composite of relation}}
Note that this result holds for any $\RR \subseteq S \times T$, and does not require that $\struct {S, \RR}$ necessarily be a relational structure.
{{begin-eqn}}
{{eqn | l = \tuple {a, b}
      | o = \in
      | r =\RR^{-1} \circ \RR
      | c =
}}
{{eqn | ll= \leadsto
      | q = \exists c \in T
      | l = \tuple {a, c}
      | o = \in
      | r = \RR
      | c = {{Defof|Composition of Relations}}
}}
{{eqn | lo= \land
      | l = \tuple {c, b}
      | o = \in
      | r = \RR^{-1}
}}
{{eqn | ll= \leadsto
      | q = \exists c \in T
      | l = \tuple {b, c}
      | o = \in
      | r = \RR 
      | c = {{Defof|Inverse Relation}}
}}
{{eqn | lo= \land
      | l = \tuple {c, a}
      | o = \in
      | r = \RR^{-1}
}}
{{eqn | ll= \leadsto
      | l = \tuple {b, a}
      | o = \in
      | r = \RR^{-1} \circ \RR
      | c = {{Defof|Composition of Relations}}
}}
{{end-eqn}}
Thus $\tuple {a, b} \in \RR^{-1} \circ \RR \implies \tuple {b, a} \in \RR^{-1} \circ \RR$ and thus $\RR^{-1} \circ \RR$ is symmetric.
As $\RR = \paren {\RR^{-1} }^{-1}$ from Inverse of Inverse Relation, it follows that $\RR \circ \RR^{-1} = \paren {\RR^{-1} }^{-1} \circ \RR^{-1}$ is likewise a symmetric relation.
The domain of $\RR^{-1} \circ \RR$ is $S$ from Domain of Composite Relation, as is its codomain from Codomain of Composite Relation and the definition of Inverse Relation.
Similarly, the codomain of $\RR \circ \RR^{-1}$ is $T$, as is its domain.
This completes the proof.
{{Qed}}
Category:Symmetric Relations
Category:Composite Relations
m10chvkici20ztfuehrmpnw59i8p1er
Theorem: Inverse of Many-to-One Relation is One-to-Many

The inverse of a many-to-one relation is a one-to-many relation, and vice versa.

Proof:
From the definition, a many-to-one relation $\RR \subseteq S \times T$ is such that:
:$\RR \subseteq S \times T: \forall x \in \Dom \RR: \tuple {x, y_1} \in \RR \land \tuple {x, y_2} \in \RR \implies y_1 = y_2$
Also from the definition, a one-to-many relation $\RR \subseteq S \times T$ is such that:
:$\RR \subseteq S \times T: \forall y \in \Img \RR: \tuple {x_1, y} \in \RR \land \tuple {x_2, y} \in \RR \implies x_1 = x_2$
The inverse of a relation $\RR$ is defined as:
:$\RR^{-1} = \set {\tuple {t, s}: \tuple {s, t} \in \RR}$
Also from the definition of inverse relation, we have that:
:$\Dom \RR = \Rng {\RR^{-1} }$
:$\Rng \RR = \Dom {\RR^{-1} }$
So, let $\RR$ be a many-to-one relation.
Putting the above all together, we have:
:$\RR^{-1} \subseteq T \times S: \forall x \in \Img {\RR^{-1} }: \tuple {y_1, x} \in \RR^{-1} \land \tuple {y_2, x} \in \RR^{-1} \implies y_1 = y_2$
and it can be seen that $\RR^{-1}$ is one-to-many.
Similarly, let $\RR$ be a one-to-many relation.
This gives us:
:$\RR^{-1} \subseteq T \times S: \forall y \in \Dom {\RR^{-1} }: \tuple {y, x_1} \in \RR^{-1} \land \tuple {y, x_2} \in \RR^{-1} \implies x_1 = x_2$
and it can be seen that $\RR^{-1}$ is many-to-one.
{{qed}}
Category:Inverse Relations
dfoiol7hvnhemrsko1ngk6ppfsnvtvy
Theorem: One-to-Many Relation Composite with Inverse is Coreflexive

Let $\RR \subseteq S \times S$ be a relation which is one-to-many.
Then the composite of $\RR$ with its inverse is a coreflexive relation:
:$\RR^{-1} \circ \RR \subseteq \Delta_X$
{{refactor|This is a separate result.|level = basic}}
That is, by Relation is Symmetric and Antisymmetric iff Coreflexive, $\RR^{-1} \circ \RR$ is both symmetric and antisymmetric.

Proof:
As $\RR$ is one-to-many, it follows from Inverse of Many-to-One Relation is One-to-Many that $\RR^{-1}$ is many-to-one.
Let $\tuple {x, z} \in \RR^{-1} \circ \RR$.
Then:
:$\exists y \in S: \tuple {x, y} \in \RR, \tuple {y, z} \in \RR^{-1}$
As $\tuple {x, y} \in \RR$, from the definition of inverse relation:
:$\tuple {y, x} \in \RR^{-1}$
As $\RR^{-1}$ is many-to-one:
:$\tuple {y, z} = \tuple {y, x}$
Thus if $\tuple {x, z} \in \RR^{-1} \circ \RR$, it follows that:
:$\tuple {x, z} = \tuple {x, x}$
Thus:
:$\RR^{-1} \circ \RR \subseteq \Delta_X$
The result follows by definition of coreflexive relation.
{{Qed}}
Category:Coreflexive Relations
gxk71yp463uwm1wdos8klc0ei1a5f0z
Theorem: Element in its own Equivalence Class

Let $\RR$ be an equivalence relation on a set $S$.
Then every element of $S$ is in its own $\RR$-class:
:$\forall x \in S: x \in \eqclass x \RR$

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \tuple {x, x}
      | o = \in
      | r = \RR
      | c = {{Defof|Equivalence Relation}}: $\RR$ is Reflexive
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \eqclass x \RR
      | c = {{Defof|Equivalence Class}}
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence Class of Element is Subset

Let $\RR$ be an equivalence relation on a set $S$.
The $\RR$-class of every element of $S$ is a subset of the set the element is in:
:$\forall x \in S: \eqclass x \RR \subseteq S$

Proof:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = \eqclass x \RR
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {x, y}
      | o = \in
      | r = \RR
      | c = {{Defof|Equivalence Class}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = S \land y \in S
      | c = {{Defof|Relation}}
}}
{{eqn | ll= \leadsto
      | l = \eqclass x \RR
      | o = \subseteq
      | r = S
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{Qed}}
Category:Equivalence Classes
mk6p7s2kmdqu8xev1qi7xf3e4vyrgiv
Theorem: Equivalence Class is not Empty

Let $\RR$ be an equivalence relation on a set $S$.
Then no $\RR$-class is empty.

Proof:
{{begin-eqn}}
{{eqn | q = \forall \eqclass x \RR \subseteq S: \exists x \in S
      | l = x
      | o = \in
      | r = \eqclass x \RR
      | c = {{Defof|Equivalence Class}}
}}
{{eqn | ll= \leadsto
      | l = \eqclass x \RR
      | o = \ne
      | r = \O
      | c = {{Defof|Empty Set}}
}}
{{end-eqn}}
Theorem: Handshake Lemma

Let $G$ be a $\tuple {p, q}$-undirected graph, which may be a multigraph or a loop-graph, or both.
Let $V = \set {v_1, v_2, \ldots, v_p}$ be the vertex set of $G$.
Then:
:$\ds \sum_{i \mathop = 1}^p \map {\deg_G} {v_i} = 2 q$
where $\map {\deg_G} {v_i}$ is the degree of vertex $v_i$.
That is, the sum of all the degrees of all the vertices of an graph is equal to twice its size.
This result is known as the '''Handshake Lemma''' or '''Handshaking Lemma'''.

Proof:
In the notation $\tuple {p, q}$-graph, $p$ is its order and $q$ its size.
That is, $p$ is the number of vertices in $G$, and $q$ is the number of edges in $G$.
Each edge is incident to exactly two vertices.
The degree of each vertex is defined as the number of edges to which it is incident.
So when we add up the degrees of all the vertices, we are counting all the edges of the graph twice.
{{qed}}
Theorem: Equivalence Class holds Equivalent Elements

Let $\RR$ be an equivalence relation on a set $S$.
Then:
:$\tuple {x, y} \in \RR \iff \eqclass x \RR = \eqclass y \RR$

Proof:
=== Necessary Condition ===
First we prove that $\tuple {x, y} \in \RR \implies \eqclass x \RR = \eqclass y \RR$.
Suppose:
: $\tuple {x, y} \in \RR: x, y \in S$
Then:
{{begin-eqn}}
{{eqn | l = z
      | o = \in
      | r = \eqclass x \RR
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {x, z}
      | o = \in
      | r = \RR
      | c = {{Defof|Equivalence Class}}
}}
{{eqn | ll= \leadsto
      | l = \tuple {z, x}
      | o = \in
      | r = \RR
      | c = {{Defof|Equivalence Relation}}: $\RR$ is symmetric
}}
{{eqn | ll= \leadsto
      | l = \tuple {z, y}
      | o = \in
      | r = \RR
      | c = {{Defof|Equivalence Relation}}: $\RR$ is transitive
}}
{{eqn | ll= \leadsto
      | l = \tuple {y, z}
      | o = \in
      | r = \RR
      | c = {{Defof|Equivalence Relation}}: $\RR$ is symmetric
}}
{{eqn | ll= \leadsto
      | l = z
      | o = \in
      | r = \eqclass y \RR
      | c = {{Defof|Equivalence Class}}
}}
{{end-eqn}}
So:
:$\eqclass x \RR \subseteq \eqclass y \RR$
Now:
{{begin-eqn}}
{{eqn | l = \tuple {x, y} \in \RR
      | o = \implies
      | r = \eqclass x \RR \subseteq \eqclass y \RR
      | c = (see above)
}}
{{eqn | l = \tuple {x, y} \in \RR
      | o = \implies
      | r = \tuple {y, x} \in \RR
      | c = {{Defof|Equivalence Relation}}: $\RR$ is symmetric
}}
{{eqn | o = \leadsto
      | r = \eqclass y \RR \subseteq \eqclass x \RR
      | c = from above
}}
{{eqn | o = \leadsto
      | r = \eqclass y \RR = \eqclass x \RR
      | c = {{Defof|Set Equality}}
}}
{{end-eqn}}
... so we have shown that:
:$\tuple {x, y} \in \RR \implies \eqclass x \RR = \eqclass y \RR$
{{qed|lemma}}
=== Sufficient Condition ===
Next we prove that $\eqclass x \RR = \eqclass y \RR \implies \tuple {x, y} \in \RR$.
By definition of set equality:
:$\eqclass x \RR = \eqclass y \RR$
means:
:$\paren {x \in \eqclass x \RR \iff x \in \eqclass y \RR}$
So by definition of equivalence class:
:$\tuple {y, x} \in \RR$
Hence by definition of equivalence relation: $\RR$ is symmetric
:$\tuple {x, y} \in \RR$
So we have shown that
:$\eqclass x \RR = \eqclass y \RR \implies \tuple {x, y} \in \RR$
Thus, we have:
{{begin-eqn}}
{{eqn | l = \tuple {x, y} \in \RR
      | o = \implies
      | r = \eqclass x \RR = \eqclass y \RR
      | c = 
}}
{{eqn | l = \eqclass x \RR = \eqclass y \RR
      | o = \implies
      | r = \tuple {x, y} \in \RR
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
So by equivalence:
:$\tuple {x, y} \in \RR \iff \eqclass x \RR = \eqclass y \RR$
{{qed}}
Theorem: Equivalence Classes are Disjoint

Let $\RR$ be an equivalence relation on a set $S$.
Then all $\RR$-classes are pairwise disjoint:
:$\tuple {x, y} \notin \RR \iff \eqclass x \RR \cap \eqclass y \RR = \O$

Proof:
First we show that:
:$\tuple {x, y} \notin \RR \implies \eqclass x \RR \cap \eqclass y \RR = \O$
Suppose two $\RR$-classes are ''not'' disjoint:
{{begin-eqn}}
{{eqn | l = \eqclass x \RR \cap \eqclass y \RR \ne \O
      | o = \leadsto
      | r = \exists z: z \in \eqclass x \RR \cap \eqclass y \RR
      | c = {{Defof|Empty Set}}
}}
{{eqn | o = \leadsto
      | r = \exists z: z \in \eqclass x \RR \land z \in \eqclass y \RR
      | c = {{Defof|Set Intersection}}
}}
{{eqn | o = \leadsto
      | r = \exists z: \paren {\tuple {x, z} \in \RR} \land \paren {\tuple {y, z} \in \RR}
      | c = {{Defof|Equivalence Class}}
}}
{{eqn | o = \leadsto
      | r = \exists z: \paren {\tuple {x, z} \in \RR} \land \paren {\tuple {z, y} \in \RR}
      | c = {{Defof|Symmetric Relation}}: $\RR$ is symmetric
}}
{{eqn | o = \leadsto
      | r = \tuple {x, y} \in \RR
      | c = {{Defof|Transitive Relation}}: $\RR$ is transitive
}}
{{end-eqn}}
So:
:$\eqclass x \RR \cap \eqclass y \RR \ne \O \implies \tuple {x, y} \in \RR$
By the Rule of Transposition:
:$\tuple {x, y} \notin \RR \implies \eqclass x \RR \cap \eqclass y \RR = \O$
{{qed|lemma}}
Now we show that:
:$\eqclass x \RR \cap \eqclass y \RR = \O \implies \tuple {x, y} \notin \RR$
Suppose:
:$\tuple {x, y} \in \RR$.
Then:
{{begin-eqn}}
{{eqn | o = 
      | r = y \in \eqclass y \RR
      | c = {{Defof|Equivalence Class}}
}}
{{eqn | o = 
      | r = \tuple {x, y} \in \RR
      | c = by hypothesis
}}
{{eqn | o = \leadsto
      | r = y \in \eqclass x \RR
      | c = {{Defof|Equivalence Class}}
}}
{{eqn | o = \leadsto
      | r = y \in \eqclass x \RR \land y \in \eqclass y \RR
      | c = Rule of Conjunction
}}
{{eqn | o = \leadsto
      | r = y \in \eqclass x \RR \cap \eqclass y \RR
      | c = {{Defof|Set Intersection}}
}}
{{eqn | o = \leadsto
      | r = \eqclass x \RR \cap \eqclass y \RR \ne \O
      | c = {{Defof|Empty Set}}
}}
{{end-eqn}}
So:
:$\tuple {x, y} \in \RR \implies \eqclass x \RR \cap \eqclass y \RR \ne \O$
By the Rule of Transposition:
:$\eqclass x \RR \cap \eqclass y \RR = \O \implies \paren {x, y} \notin \RR$
Using the rule of Biconditional Introduction on these results:
:$\eqclass x \RR \cap \eqclass y \RR = \O \iff \paren {x, y} \notin \RR$
and the proof is complete.
Theorem: Equivalence Classes are Disjoint

Let $\RR$ be an equivalence relation on a set $S$.
Then all $\RR$-classes are pairwise disjoint:
:$\tuple {x, y} \notin \RR \iff \eqclass x \RR \cap \eqclass y \RR = \O$

Proof:
Suppose that for $x, y \in S$:
:$\eqclass x \RR \cap \eqclass y \RR \ne \O$
Let:
:$z \in \eqclass x \RR$
:$z \in \eqclass y \RR$
Then by definition of equivalence class:
:$\tuple {x, z} \in \RR$
:$\tuple {y, z} \in \RR$
Let $c \in \eqclass x \RR$.
That is:
:$\tuple {x, c} \in \RR$
By definition of equivalence relation, $\RR$ is symmetric so:
:$\tuple {z, x} \in \RR$
By definition of equivalence relation, $\RR$ is transitive so:
:$\tuple {z, x} \in \RR \land \tuple {x, c} \in \RR \implies \tuple {z, c} \in \RR$
and
:$\tuple {y, z} \in \RR \land \tuple {z, c} \in \RR \implies \tuple {y, c} \in \RR$
So we have $c \in \eqclass y \RR$.
By definition of subset:
:$\eqclass x \RR \subseteq \eqclass y \RR$
Similarly, let $c \in \eqclass y \RR$.
That is:
:$\tuple {y, c} \in \RR$
By definition of equivalence relation, $\RR$ is symmetric so:
:$\tuple {z, y} \in \RR$
By definition of equivalence relation, $\RR$ is transitive so:
:$\tuple {z, y} \in \RR \land \tuple {y, c} \in \RR \implies \tuple {z, c} \in \RR$
and
:$\tuple {x, z} \in \RR \land \tuple {z, c} \in \RR \implies \tuple {x, c} \in \RR$
So we have $c \in \eqclass x \RR$.
By definition of subset:
:$\eqclass y \RR \subseteq \eqclass x \RR$
That is:
:$\eqclass x \RR \subseteq \eqclass y \RR$
and
:$\eqclass y \RR \subseteq \eqclass x \RR$
By definition of set equality:
:$\eqclass x \RR = \eqclass y \RR$
Thus:
:$\eqclass x \RR \cap \eqclass y \RR \ne \O \implies \eqclass x \RR = \eqclass y \RR$
and the result follows.
{{qed}}
Theorem: Fundamental Theorem on Equivalence Relations

Let $\RR \subseteq S \times S$ be an equivalence on a set $S$.
Then the quotient set $S / \RR$ of $S$ by $\RR$ forms a partition of $S$.

Proof:
To prove that $S / \RR$ is a partition of $S$, we have to prove:
:$(1): \quad \ds \bigcup {S / \RR} = S$
:$(2): \quad \eqclass x \RR \ne \eqclass y \RR \iff \eqclass x \RR \cap \eqclass y \RR = \O$
:$(3): \quad \forall \eqclass x \RR \in S / \RR: \eqclass x \RR \ne \O$
Taking each proposition in turn:
Theorem: Equivalence Class is Unique

Let $\RR$ be an equivalence relation on $S$.
For each $x \in S$, the one and only one $\RR$-class to which $x$ belongs is $\eqclass x \RR$.

Proof:
This follows directly from the Fundamental Theorem on Equivalence Relations: the set of $\RR$-classes forms a partition of $S$.
{{qed}}
Theorem: Equivalence Class Equivalent Statements

Let $\RR$ be an equivalence relation on $S$.
Let $x, y \in S$.
{{TFAE}}
:$(1): \quad x$ and $y$ are in the same $\RR$-class
:$(2): \quad \eqclass x \RR = \eqclass y \RR$
:$(3): \quad x \mathrel \RR y$
:$(4): \quad x \in \eqclass y \RR$
:$(5): \quad y \in \eqclass x \RR$
:$(6): \quad \eqclass x \RR \cap \eqclass y \RR \ne \O$

Proof:
=== $(1)$ Equivalent to $(2)$ ===
{{:Equivalence Class Equivalent Statements/1 iff 2}}
Theorem: Relation Induced by Partition is Equivalence

Let $\mathbb S$ be a partition of a set $S$.
Let $\RR$ be the relation induced by $\mathbb S$.
Then:
:$(1): \quad \RR$ is unique
:$(2): \quad \RR$ is an equivalence relation on $S$.
Hence $\mathbb S$ is the quotient set of $S$ by $\RR$, that is:
:$\mathbb S = S / \RR$

Proof:
From the definition of Relation Induced by Partition, we define the relation $\RR$ on $S$ by:
:$\RR = \set {\tuple {x, y}: \paren {\exists T \in \mathbb S: x \in T \land y \in T} }$