\begin{definition}[Definition:Class/Zermelo-Fraenkel]
Denote with $\textrm{ZF}$ the language of set theory endowed with the Zermelo-Fraenkel axioms.
A '''class''' in $\textrm{ZF}$ is a formal vehicle capturing the intuitive notion of a class, namely a collection of all sets such that a particular condition $P$ holds.
In $\textrm{ZF}$, '''classes''' are written using class builder notation:
:$\set {x : \map P x}$
{{Questionable|Wouldn't you need the Class Comprehension Axiom for this?}}
where $\map P x$ is a statement containing $x$ as a free variable.  
More formally, a '''class''' $\set {x: \map P x}$ serves to define the following definitional abbreviations involving the membership symbol:
{{begin-eqn}}
{{eqn | l = y \in \set {x: \map P x}
      | o = \text{for}
      | r = \map P y
}}
{{eqn | l = \set {x: \map P x} \in y
      | o = \text{for}
      | r = \exists z \in y: \forall x: \paren {x \in z \iff \map P x}
}}
{{eqn | l = \set {x: \map P x} \in \set {y: \map Q y}
      | o = \text{for}
      | r = \exists z: \paren {\map Q z \land \forall x: \paren {x \in z \iff \map P x} }
}}
{{end-eqn}}
where:
:$x, y ,z$ are variables of $\textrm{ZF}$
:$P, Q$ are propositional functions.
Through these "rules", every statement involving $\set {x: \map P x}$ can be reduced to a simpler statement involving only the basic language of set theory.
This definition "overloads" the membership symbol $\in$ since its operands could now be either sets or '''classes'''.
That such does not lead to ambiguity is proved on Class Membership Extension of Set Membership.
{{proofread}}
\end{definition}