---
tag: D96K8S8R61
kind: concept
name: Axiom schema of replacement
msc: ["03E30"]
uses: [0HE5WDQ9FJ, 0EPAT51DXQ, 0BSJ7RQ9BW, 0YSCSX5YZC]
sources:
  - url: https://en.wikipedia.org/wiki/Axiom_schema_of_replacement
same_as:
  wikidata: Q1361825
  wikipedia: Axiom schema of replacement
---

## Summary

The axiom schema of replacement is a list of axioms of [[Zermelo–Fraenkel set theory|0HE5WDQ9FJ]], one for each formula.
It says that the image of a [[set|0BSJ7RQ9BW]] under a definable [[function|0EPAT51DXQ]] is again a set.
Fraenkel and Skolem proposed it in 1922 as an addition to Zermelo's axioms.
It is needed to build large sets such as $\aleph_\omega$ and to define functions on [[ordinals|0YSCSX5YZC]] by transfinite recursion.

## Explanations

### L1 human

Suppose you have a set, and a rule that assigns to each element of it a unique object.
Replacement says that the objects you get form a set too.
You replace each element by its image, and the result is still a set.
For example, from the set of natural numbers $\N$ and the rule $n \mapsto \mathcal{P}^n(\N)$, the $n$-fold power set, one gets the set $\set{\N, \mathcal{P}(\N), \mathcal{P}(\mathcal{P}(\N)), \dots}$.
Without replacement, this set cannot be proved to exist.