How can I deduce the existence of the image set $f(S)$ from the axiom of specification

Question

Let $f:X\to Y$ be some function and $S\subseteq X$ a subset of its domain. It is clear that the image set $f(S)$ exists, as

$$f(S):=\{f(x)\mid x\in S\}=\{y\mid \exists x\in S(f(x)=y)\},$$

and for each $x\in S$, there is at most one $y$ for which $\exists x\in S(f(x)=y)$ holds. Thus, by the axiom of replacement, this set $f(S)$ exists so that $$z\in f(S)=\{y\mid \exists x\in S(f(x)=y)\}\iff (z\in S \land\exists x\in S(f(x)=z)).$$ Is it possible to deduce the existance of $f(S)$ from the axiom of specification? (because the page on which this axiom appears in my book is not available in the google preview, I will include it here):

Axiom. Let $A$ be a set and $P(x)$ some property pertaining to $x\in A$. Then there exists a set $\{x\in A\mid P(x)\}$ such that for any object $y$, $$y\in\{x\in A\mid P(x)\}\iff (y\in A\land P(x))$$

Answer 1

Following the wikipedia entry on the axiom schema of specification (here) where we use $f$ and $S$ as unbound parameters, we can write

$$f[S] = \{ y \in Y: \exists s: s \in S \land y=f(s) \}$$

so we use $\phi(S,f,y) = (\exists s \in S: (s \in S) \land y = f(s))$ as the formula. The subformula $y=f(s)$ can be more primitively written as $(s,y) \in f$ if you prefer to work in a language with only $\in$. So then we use $$\phi(S,f,y) = \exists s \in S: (s \in S) \land ((s,y) \in f)$$ instead.

Answer 2

Of course, just write

$$f[S] = \{ y \in Y : (\exists x \in S) \, y = f(x) \}.$$

Any use of the axiom of replacement can be replaced (:p) with the use of the axiom of specification unless the codomain of our function is not known to be a set beforehand. Since here we have that $Y$ is a set (which it is because we can extract it from $f$ with set-theoretical operations*), we can do it.

*If fact, what we can extract is the very image itself, not the codomain, but we wanted to use the axiom of specification somehow, so here it is.

Answer 3

Even if you don't know that $f:X\to Y$ for known sets $X$ and $Y$, you can do it with Specification, assuming that you're modeling relations and functions as sets of Kuratowski ordered pairs. Namely, in that case every possible value of $f$ is in $\bigcup\bigcup f$, so you can write $$ f(S) = \{ y\in\bigcup\bigcup f \mid \exists x\in S: y=f(x) \}$$