Axiom:Axiom of Replacement

From ProofWiki
Jump to navigation Jump to search

Axiom

For any function $f$ and subset $S$ of the domain of $f$, there is a set containing the image $f \left({S}\right)$.

More formally, let us express this as follows:


Let $P \left({y, z}\right)$ be a propositional function, which determines a function.

That is, we have $\forall y: \exists x: \forall z: \left({ P \left({y, z}\right) \iff x = z }\right)$.

Then we state as an axiom:

$\forall w: \exists x: \forall y: \left({y \in w \implies \left({ \forall z: \left({ P \left({y, z}\right) \implies z \in x }\right) }\right) }\right)$


Alternatively, the two above statements may be combined into a single (somewhat unwieldy) expression:

$\left({ \forall y: \exists x: \forall z: \left({ P \left({y, z}\right) \implies x = z }\right) }\right) \implies \forall w: \exists x: \forall y: \left({y \in w \implies \forall z: \left({ P \left({y, z}\right) \implies z \in x }\right) }\right)$


Sources