Suppose that I connect syntactically the first order logic with ZFC by changing $\forall x \phi(x)$ by if $x$ is a set then $\phi (x)$ stating that x is not free in "if $x$ is a set then $\phi (x)$" in the same sense of "$\forall x \phi(x)$", use this change to eliminate the existential quantifier and call the new language ZFC'. I understand that ZFC' is not longer under first order logic so it may not make sense to talk about semantic using model theory. My question is: intuitively everything that can be proved in ZFC (without using semantic) can be proved in ZFC' and vice versa? For me, the answer is yes but I am not sure.
The idea is not substitute a symbol ($\forall$) for other with same meaning because the yes answer would be trivial. The intended meaning for "if $x$ is a set then $\phi (x)$" is "if $x\in U$ then $\phi (x)$" where $U$ is the universe that does not exist in ZFC.