Equivalence of Formulations of Axiom of Replacement

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

This theorem requires a proof. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by crafting such a proof. 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 {{ProofWanted}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

Sources

• 2010: Raymond M. Smullyan and Melvin Fitting: Set Theory and the Continuum Problem (revised ed.) ... (previous) ... (next): Chapter $6$: Order Isomorphism and Transfinite Recursion: $\S 3$ The axiom of substitution: Exercise $3.1$