Axiom schema of replacement

Provisional page grade: A*

This page is provisional

This page is provisional and the information it contains may change before this notice is removed (in a backwards incompatible way). This usually means the content is from one source and that source isn't the most formal, or there are many other forms floating around. It is on a to-do list for being expanded.The message provided is:

Needs:

• Infobox
• Apart of what set theories?
• Anything it requires as a precursor?
• Corollaries / use

$\newcommand{\limplies}[0]{\rightarrow} \newcommand{\liff}[0]{\leftrightarrow}$

Definition

Let $\varphi(a,b,p)$ be a formula where $a$ and $b$ are free variables but $p$ is a parameter (or a parameter pack) and describes a function between classes.

The axiom schema of replacement posits that if $F$ is some class function then for all sets $X$, $F(X)$ - the image of $X$ under $F$ - denoted $F(X)$ is also a set.

We state it formally as follows:

• $\Big(\underbrace{\forall x\forall y\forall z\big[\big(\varphi(x,y,p)\wedge\varphi(x,z,p)\big)\limplies y\eq z\big]}_{\text{if }(a,b)\in f\iff\varphi(a,b,p)\text{ then }f\text{ acts like a function relation} }\Big)$ $\limplies$ $\Big(\underbrace{\forall X\exists Y\forall y\big[y\in Y\liff\exists x[x\in X\wedge\varphi(x,y,p)]\big]}_{y\in Y\iff\text{the 'image' of }x\text{ under the 'function' is }y }\Big)$
  • By rewriting for-all and exists within set theory we can make a small change to the $\exists x$ part:
    • $\Big(\forall x\forall y\forall z\big[\big(\varphi(x,y,p)\wedge\varphi(x,z,p)\big)\limplies y\eq z\big]\Big)$ $\limplies$ $\Big(\forall X\exists Y\forall y\big[y\in Y\liff\exists x\in X[\varphi(x,y,p)]\big]\Big)$