# Category:Zermelo-Fraenkel Class Theory

This category contains results about **classes in ZF set theory**.

Definitions specific to this category can be found in Definitions/Zermelo-Fraenkel Class Theory.

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

where $\map P x$ is a well-formed formula 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 well-formed formulas.

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.

## Subcategories

This category has the following 2 subcategories, out of 2 total.

## Pages in category "Zermelo-Fraenkel Class Theory"

The following 11 pages are in this category, out of 11 total.