In ZFC if $x\in \{y\in z:\phi\}$ I think it is safe to conclude that $x\in z \wedge \phi[y/x]$ but since $\phi[y/x]$ is not part of the language what is the logical equivalent that is part of the language?
In the same manner $(\forall x:\phi) \Rightarrow \phi[x/y]$ but again $\phi[x/y]$ is not part of the language, could it be extended to include it? (I doubt since in $\phi[x/y]$ "x" is a label and is directly bound to the physical representation of $\phi$)?
Okay, another try, after this one: Formulation of axiom of induction?
Reframing the problem
I'm still thinking you got something confused about meta-statements and statements in the object-language. Since it is the same for me from time to time I might be just biased. But I hope to enable you to clarify the question for yourself at least.
The statement
$$\text{In ZFC if }x \in \{ y \in z : \phi \}\text{, then }x \in z \wedge \phi[y/x]$$
is clearly a meta-statement. Even if you formalize $\phi[y/x]$ within the object-language it is still a meta statement since you're talking about an arbitrary $\phi$!
So, say $\phi[y/x]$ was a sentence in the object-language for every $\phi$. Then the statement
$$x\in\{y\in z : \phi \} \to x \in z \wedge \phi[y/x]$$
would be still a meta statement, because in fact it says:
$$\text{for all formula }\phi\text{ it holds that } x\in\{y\in z : \phi \} \to x \in z \wedge \phi[y/x].$$
The part which uses mathematical symbols is still meta statement if you look twice, since it is a scheme.
Comments
If you, though, take a certain instance, i.e. a specific formula for that $\phi$ you get a specific formula $\phi[y/x]$ and hence you're able to proof it using no meta mumbo jumbo but at the cost of the generality.
You might have come across exercises which tell you to prove $\phi \vee \neg \phi$ or such. In fact, even if you use a calculus, you're still proving it encapsulated within meta: for every $\phi$ show that $\phi \vee \neg\phi$. Now, what you are doing is meta generialization: Let $\phi$ be any formula, then ...
Another way you might consider is encoding "x is free in $\phi$" into the language of ZFC. Something like Gödel numbers for formulae; such that you can talk about an arbitrary formula within the object language by quantifying over all Gödel numbers which represent a valid formula. I've no clue if this is possible though. But my intuition tells me that this is not what you're looking for. I might be wrong though.