Axiom:Axiom of Replacement

From ProofWiki
Jump to navigation Jump to search


Set Theory

For every mapping $f$ and subset $S$ of the domain of $f$, there exists a set containing the image $f \sqbrk S$.

More formally, let us express this as follows:

Let $\map P {x, z}$ be a propositional function, which determines a mapping.

That is, we have:

$\forall x: \exists ! y : \map P {x, y}$.

Then we state as an axiom:

$\forall A: \exists B: \forall y: \paren {y \in B \iff \exists x \in A : \map P {x, y} }$

Class Theory

For every mapping $f$ and set $x$ in the domain of $f$, the image $f \sqbrk x$ is a set.


$\forall Y: \map {\text{Fnc}} Y \implies \forall x: \exists y: \forall u: u \in y \iff \exists v: \tuple {v, u} \in Y \land v \in x$


$\map {\text{Fnc}} X := \forall x, y, z: \tuple {x, y} \in X \land \tuple {x, z} \in X \implies y = z$

and the notation $\tuple {\cdot, \cdot}$ is understood to represent Kuratowski's formalization of ordered pairs.

Also known as

The axiom of replacement is also known as the axiom of substitution.

Also see

  • Results about the Axiom of Replacement can be found here.

Historical Note

The axiom of replacement was added to the axioms of Zermelo set theory by Abraham Halevi Fraenkel, and also independently by Thoralf Albert Skolem.

The resulting system of axiomatic set theory is now referred to as Zermelo-Fraenkel Set Theory.