User:Dfeuer/Axiom of Replacement/Gödel

Axiom

$\forall x, A: \paren {\map {\mathfrak {Un} } A \implies \exists y: \forall v: \paren {v \in y \iff \exists u: \paren {u \in x \land \tuple {u, v} \in A} } }$

where $\map {\mathfrak {Un} } A \iff \forall u, v, w: \paren {\tuple {u, v} \in A \land \tuple {u, w} \in A \implies v = w }$.

That is, for each set $x$ and each many-to-one relation $A$, there exists a set $y$ such that for all $v$, $v \in y$ if and only if there exists a $u \in x$ such that $\tuple {u, v} \in A$.

Remarks

Note that $A$ need not be a mapping on $x$. No assumption whatsoever is made about the domain of $A$.

Bernays and Gödel define a many-to-one relation inversely to $\mathsf{Pr} \infty \mathsf{fWiki}$. For the sake of consistency with the rest of the site, their definition of $\mathfrak{Un}$ and the statement of the axiom have been reversed.