Equivalence of Formulations of Axiom of Replacement

From ProofWiki
Jump to navigation Jump to search

Theorem

In the context of class theory, the following formulations of the Axiom of Replacement are equivalent:

Formulation 1

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


Symbolically:

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

where:

$\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.

Formulation 2

For every mapping $f$ and set $x$, the restriction $f \restriction x$ is a set.

Formulation 3

Every mapping whose domain is a set is also a set.


Proof




Sources