Axiom of replacement easy explanation

Question

Can someone explain me the axiom of replacement in easy words? I really dont get it, my book says What i understand from this is that for every set $x$ there is another set $y$ whose members are the elements $y'$ that satisfy the formula $\phi(x',y')$ when $x'$ exists, and $y'$ has to be unique. I don't see anything illuminating in this, the axiom of separation sounds very similar too, can you guys please make my ideas a little clearer maybe using a simple example or something? And what is a class function? Thanks!

Answer 1

It's easy if you start from a stronger version.

For every function $F$ defined on the class of sets, and for every $x$, $\{F(a)\mid a\in x\}$ is a set.

Alternatively, we can simply require that $F\restriction x$ is a set. But this requires us to first choose a way to encode functions as sets (i.e. agree on coding ordered pairs in a certain way).

Do note that we normally define a function as a set with certain properties. This would render this axiom trivial. The idea is that $F$ is a class function, it is a function on the entire universe, that is, it is a class, which is a function. Or at the very least, we do not need to assume that this function is in fact a set.

But this axiom quantifies over functions on the class of all sets, which would be a second-order quantification. So the first-order corresponding axiom is a schema that says: if $\varphi$ defines a function $F$, then the image of every set is a set.

But since "$\varphi$ defines a function" is somehow unclear if you want to be very formal, we spell it out: for every $a\in x$ there exists a unique $y$ such that $\varphi(a,y)$ holds.

Now we may notice that we don't need to say that $\varphi$ defines a function on the entire class of sets: if $\varphi$ defines a function on a set $x$, then the image of $x$ under that function is a set.

We can then notice also that we may want to include parameters, and so allow parameters in the formula.

But all of this is besides the point. The point is that if $F$ is a function, which in the first-order case means that there is a formula which defines this function, then the image of a set under $F$ is a set as well.