# Definition:Class/Zermelo-Fraenkel

This article needs to be linked to other articles.NGBYou can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{MissingLinks}}` from the code. |

## Definition

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}$

The validity of the material on this page is questionable.Wouldn't you need the Class Comprehension Axiom for this?You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by resolving the issues.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Questionable}}` from the code.If you would welcome a second opinion as to whether your work is correct, add a call to `{{Proofread}}` the page. |

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:

\(\ds y \in \set {x: \map P x}\) | \(\text{for}\) | \(\ds \map P y\) | ||||||||||||

\(\ds \set {x: \map P x} \in y\) | \(\text{for}\) | \(\ds \exists z \in y: \forall x: \paren {x \in z \iff \map P x}\) | ||||||||||||

\(\ds \set {x: \map P x} \in \set {y: \map Q y}\) | \(\text{for}\) | \(\ds \exists z: \paren {\map Q z \land \forall x: \paren {x \in z \iff \map P x} }\) |

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.

This page needs proofreading.Please check it for mathematical errors.If you believe there are none, please remove `{{Proofread}}` from the code.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Proofread}}` from the code. |

### Class Variables

In deriving general results about $\textrm{ZF}$ which mention **classes**, it is often convenient to have **class variables**, which denote an arbitrary **class**.

By convention, these variables are taken on $\mathsf{Pr} \infty \mathsf{fWiki}$ to be the (start of) the capital Latin alphabet, i.e. $A, B, C$, and so on.

## Caution

Unlike in von Neumann-Bernays-GĂ¶del set theory, it is prohibited to quantify over **classes**.

That is, expressions like:

- $\forall A: \map P A$

are ill-defined; admitting them without further consideration would lead us to Russell's Paradox.