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

[ilmath]\newcommand{\limplies}[0]{\rightarrow} \newcommand{\liff}[0]{\leftrightarrow} [/ilmath]

Definition

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

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

We state it formally as follows:

• [ilmath]\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)[/ilmath] [ilmath]\limplies[/ilmath] [ilmath]\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)[/ilmath]
  • By rewriting for-all and exists within set theory we can make a small change to the [ilmath]\exists x[/ilmath] part:
    • [ilmath]\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)[/ilmath] [ilmath]\limplies[/ilmath] [ilmath]\Big(\forall X\exists Y\forall y\big[y\in Y\liff\exists x\in X[\varphi(x,y,p)]\big]\Big)[/ilmath]