The Equivalence Class of an Element under an Equivalence Relation

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, let $a$ be a set, $R$ an equivalence relation on $a$ and $u\in a$, and write $u\,R\,v$ for $(u,v)\in R$ as in Relations, Domain, Range, Inverse and Composition §relation.

¶ The equivalence class of $u$ under $R$ is the class

$$[u]_{R}=\{v\in a:u\,R\,v\},$$

formed by restricted class abstraction with the set parameter $u$ and the class parameter $R$; its formula $v\in a\wedge(u,v)\in R$ quantifies over set variables only, the ordered pair $(u,v)$ being a defined set symbol, so it is predicative. It is a subclass of $a$ by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted, hence a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §subclass, and by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality it is the unique set $z$ satisfying the predicative formula $\forall v\,(v\in z\Leftrightarrow(v\in a\wedge u\,R\,v))$; thus $[u]_{R}$ is a defined set symbol.