DEF-EQV. Equivalence Relation.
An equivalence relation is a binary relation that is reflexive, symmetric and transitive (DEF-RP).
DEF-EQV-CLS. Equivalence Class.
Let $\sim$ be an equivalence relation on $X$ and let $a\in X$. The equivalence class of $a$ with respect to $\sim$ is
\[[a] = \{x\in X:a\sim x\}.\]
PROP-EQV-CLS.
Let $\sim$ be an equivalence relation on $X$ and let $x$, $y\in X$. The following statements are equivalent:
- $x\sim y$.
- $[x]=[y]$.
- $x\in[y]$.
- $[x]\cap[y]\neq\varnothing$.
DEF-EQV-QUO. Quotient Set.
Let $\sim$ be an equivalence relation on $X$. The quotient set of $X$ by $\sim$, or $X$ modulo $\sim$, is the set
\[X/{\sim} = \{[x]:x\in X\}.\]