# In ZFC without a few redundant axioms, does removing the dependence of the predicate/WFF on the domain set in the replacement axiom weaken the theory

set-theory

Given ZFC without the redundant axioms of specification, empty set, and pairing (please tell me if I should be more specific about what I mean here since I'm new to ZFC, I can write down more specifically what I mean, I just thought it would clutter the question though), if we change the axiom of replacement from:

Let $$\Phi(x,y,z_1,z_2,…,z_n,S)$$ be a WFF of ZFC whose free variables are $$x,y,z_1,z_2,…,z_n,S$$. Then $$\forall z_1,…,z_n\forall S(\forall x\in S\exists!y\Phi(x,y,z_1,z_2,…,z_n,S)\implies\exists R\forall y(y\in R\iff\exists x\in S\Phi(x,y,z_1,z_2,…,z_n,S))).$$

to:

Let $$\Phi(x,y,z_1,z_2,…,z_n)$$ be a WFF of ZFC whose free variables are $$x,y,z_1,z_2,…,z_n$$. Then $$\forall z_1,…,z_n\forall S(\forall x\in S\exists!y\Phi(x,y,z_1,z_2,…,z_n)\implies\exists R\forall y(y\in R\iff\exists x\in S\Phi(x,y,z_1,z_2,…,z_n))).$$

(in the second version $$S$$ is no longer free in $$\Phi$$) is the resulting system weaker than the standard ZFC?

Ok that's a formal statement of my question, but I know that I need to provide some more context.

1. Informally, I understand the axiom schema of replacement to mean that the image of a set (the set here being $$S$$) under any definable function exists, except with two modifications: function is not used like a "function" in proper set theory here, a subset of a domain and codomain, instead the function is given as a predicate (i.e. the $$\Phi$$), and secondly in the axiom $$\Phi$$ extends to include general N-ary predicates possibly depending on some other parameters $$z_1,z_2,…,z_n$$. I don't see where the dependence on this 'domain set' $$S$$ ought to come from.

2. Finally for background, I'm self-studying this and am just interested in trying to understand this axiom a bit better. In one of my lines of thought, it seems like the $$S$$ that differs between them is irrelevant since you can take the second version with $$z_1,…,z_n,z_{n+1}$$ and then instantiate the $$n+1^\text{th}$$ parameter $$z_{n+1}$$ as $$S$$, but this seems a little sketchy for some reason. I'm not sure though that I really know how to explain why it feels sketchy without risking going off on a tangent and making the question unclear though. In any case, what the 'conventional' wisdom on this topic is would be appreciated.

First, you haven't written down the replacement scheme quite correctly. What was probably intended was $$\forall z_1,...,z_n\forall S(\forall x\in S\exists!y\;\Phi(x,y,z_1,z_2,...,z_n,S)\\\implies\exists R\forall y(y\in R\iff\exists x\in S\;\Phi(x,y,z_1,z_2,...,z_n,S)))$$ (and with a similar modification for the other version).
That aside, the idea you give in your second bullet is a correct argument that the two versions you give are equivalent. In a little more detail, let $$z_1,\ldots z_n$$ and $$S$$ be any sets. We need to show $$\forall x\in S\exists!y\;\Phi(x,y,z_1,z_2,...,z_n,S)\implies\exists R\forall y(y\in R\iff\exists x\in S\;\Phi(x,y,z_1,z_2,...,z_n,S))).$$ Per your idea, consider the an instance of the second version of replacement $$\forall z_1,...,z_{n+1}\forall S(\forall x\in S\exists!y\;\Phi(x,y,z_1,z_2,...,z_n, z_{n+1})\implies\exists R\forall y(y\in R\iff\exists x\in S\;\Phi(x,y,z_1,z_2,...,z_n, z_{n+1}))).$$ and instantiate the outer universal quantifiers as $$z_i=z_i$$ for $$i=1,\ldots n,$$ $$z_{n+1}$$ as $$S$$ and $$S$$ as $$S,$$ and then we have exactly what we needed to show.