With respect to your second question (I understand the uniqueness requirement in your questions as "being instatiatiated by abstraction terms"  ):

Suppose that $A$ is equivalent (in $ZF$) to a sentence of the form $\forall z\exists y B$, for $B$ (provably in $ZF$) absolute for transitive models of $ZF$, and that $ZFC\vdash A$.

In this case, $ZFC\vdash\forall x A^{\textbf{L}(x)}$ (where $x$ is the first variable that does not occur in $A$) if and only if (omitting the quantifier $\forall x$),

$ZFC\vdash (\forall z\exists y B)^{\textbf{L}(x)}$,

that is, if and only if

$ZFC\vdash (\forall z\in \textbf{L}(x))(\exists y\in \textbf{L}(x)) B$,

because $B$ is absolute. If this holds, then

$ZFC\vdash (x\in \textbf{L}(x))\rightarrow(\exists y\in \textbf{L}(x)) B'$

for $B'$, the formula obtained replacing the free occurrences of $z$ in $B$ by $x$. But then

$ZFC\vdash (\exists y\in \textbf{L}(x)) B'$

and, replacing back $x$ by $z$,

$ZFC\vdash (\exists y\in \textbf{L}(z)) B$.

This means that if $A$ is a theorem of $ZFC$ of the form explained above and such that $ZFC\vdash\forall x A^{\textbf{L}(x)}$, then $ZFC$ proves that given a set $z$ there exists a set $y$ in $\textbf{L}(z)$ such that $B$. Therefore, there is a composition of Godel operations applied to some elements in the transitive closure of $z$ that gives you a witness for that existence. So, even in this simple case you don't have instantiation by an abstraction term with parameter $z$, but you do have something close to it, that is a term with parameters in the transitive closure of $z$. I think that there is no way to substantially improve this.

The so-called existence axioms of set theory are classified according to this condition of being instantiated by an abstraction term or not. The axiom of choice is the example of existence axiom that is not instantiated by an abstraction term. I think that this is an inadequate condition for classifying the axioms and these and other related questions are the subject of my paper "on existence in set theory", (to appear in notre dame journal of formal logic).

With respect to your second question (I understand the uniqueness requirement in your questions as "being instatiatiated by abstraction terms"):

Suppose that $A$ is equivalent (in $\mathit{ZF}$) to a sentence of the form $\forall z\exists y B$, for $B$ (provably in $\mathit{ZF}$) absolute for transitive models of $\mathit{ZF}$, and that $\mathit{ZFC}\vdash A$.

In this case, $\mathit{ZFC}\vdash\forall x A^{\mathbf{L}(x)}$ (where $x$ is the first variable that does not occur in $A$) if and only if (omitting the quantifier $\forall x$),

$$\mathit{ZFC}\vdash (\forall z\exists y B)^{\mathbf{L}(x)},$$

that is, if and only if

$$\mathit{ZFC}\vdash (\forall z\in \mathbf{L}(x))(\exists y\in \mathbf{L}(x)) B,$$

because $B$ is absolute. If this holds, then

$$\mathit{ZFC}\vdash (x\in \mathbf{L}(x))\rightarrow(\exists y\in \mathbf{L}(x)) B'$$

for $B'$, the formula obtained replacing the free occurrences of $z$ in $B$ by $x$. But then

$$\mathit{ZFC}\vdash (\exists y\in \mathbf{L}(x)) B'$$

and, replacing back $x$ by $z$,

$$\mathit{ZFC}\vdash (\exists y\in \mathbf{L}(z)) B.$$

This means that if $A$ is a theorem of $\mathit{ZFC}$ of the form explained above and such that $\mathit{ZFC}\vdash\forall x A^{\mathbf{L}(x)}$, then $\mathit{ZFC}$ proves that given a set $z$ there exists a set $y$ in $\mathbf{L}(z)$ such that $B$. Therefore, there is a composition of Gödel operations applied to some elements in the transitive closure of $z$ that gives you a witness for that existence. So, even in this simple case you don't have instantiation by an abstraction term with parameter $z$, but you do have something close to it, that is a term with parameters in the transitive closure of $z$. I think that there is no way to substantially improve this.

The so-called existence axioms of set theory are classified according to this condition of being instantiated by an abstraction term or not. The axiom of choice is the example of existence axiom that is not instantiated by an abstraction term. I think that this is an inadequate condition for classifying the axioms and these and other related questions are the subject of my paper "On existence in set theory" in the Notre Dame journal of formal logic.

With respect to your second question (I understand the uniqueness requirement in your questions as "being instatiatiated by abstraction terms" ):

Suppose that $A$ is equivalent (in $ZF$) to a sentence of the form $\forall z\exists y B$, for $B$ (provably in $ZF$) absolute for transitive models of $ZF$, and that $ZFC\vdash A$.

In this case, $ZFC\vdash\forall x A^{\textbf{L}(x)}$ (where $x$ is the first variable that does not occur in $A$) if and only if (omitting the quantifier $\forall x$),

$ZFC\vdash (\forall z\exists y B)^{\textbf{L}(x)}$,

that is, if and only if

$ZFC\vdash (\forall z\in \textbf{L}(x))(\exists y\in \textbf{L}(x)) B$,

because $B$ is absolute. If this holds, then

$ZFC\vdash (x\in \textbf{L}(x))\rightarrow(\exists y\in \textbf{L}(x)) B'$

for $B'$, the formula obtained replacing the free occurrences of $z$ in $B$ by $x$. But then

$ZFC\vdash (\exists y\in \textbf{L}(x)) B'$

and, replacing back $x$ by $z$,

$ZFC\vdash (\exists y\in \textbf{L}(z)) B$.

This means that if $A$ is a theorem of $ZFC$ of the form explained above and such that $ZFC\vdash\forall x A^{\textbf{L}(x)}$, then $ZFC$ proves that given a set $z$ there exists a set $y$ in $\textbf{L}(z)$ such that $B$. Therefore, there is a composition of Godel operations applied to some elements in the transitive closure of $z$ that gives you a witness for that existence. So, even in this simple case you don't have instantiation by an abstraction term with parameter $z$, but you do have something close to it, that is a term with paramenters in the transitive closure of $z$. I think that there is no way to substantially improve this.

The so-called existence axioms of set theory are classified according to this condition of being instantiated by an abstraction term or not. The axiom of choice is the example of existence axiom that is not instantiated by an abstraction term. I think that this is an inadequate condition for classifying the axioms and these and other related questions are the subject of my paper "on existence in set theory", (to appear in notre dame journal of formal logic).

With respect to your second question (I understand the uniqueness requirement in your questions as "being instatiatiated by abstraction terms" ):

Suppose that $A$ is equivalent (in $ZF$) to a sentence of the form $\forall z\exists y B$, for $B$ (provably in $ZF$) absolute for transitive models of $ZF$, and that $ZFC\vdash A$.

In this case, $ZFC\vdash\forall x A^{\textbf{L}(x)}$ (where $x$ is the first variable that does not occur in $A$) if and only if (omitting the quantifier $\forall x$),

$ZFC\vdash (\forall z\exists y B)^{\textbf{L}(x)}$,

that is, if and only if

$ZFC\vdash (\forall z\in \textbf{L}(x))(\exists y\in \textbf{L}(x)) B$,

because $B$ is absolute. If this holds, then

$ZFC\vdash (x\in \textbf{L}(x))\rightarrow(\exists y\in \textbf{L}(x)) B'$

for $B'$, the formula obtained replacing the free occurrences of $z$ in $B$ by $x$. But then

$ZFC\vdash (\exists y\in \textbf{L}(x)) B'$

and, replacing back $x$ by $z$,

$ZFC\vdash (\exists y\in \textbf{L}(z)) B$.

This means that if $A$ is a theorem of $ZFC$ of the form explained above and such that $ZFC\vdash\forall x A^{\textbf{L}(x)}$, then $ZFC$ proves that given a set $z$ there exists a set $y$ in $\textbf{L}(z)$ such that $B$. Therefore, there is a composition of Godel operations applied to some elements in the transitive closure of $z$ that gives you a witness for that existence. So, even in this simple case you don't have instantiation by an abstraction term with parameter $z$, but you do have something close to it, that is a term with parameters in the transitive closure of $z$. I think that there is no way to substantially improve this.

The so-called existence axioms of set theory are classified according to this condition of being instantiated by an abstraction term or not. The axiom of choice is the example of existence axiom that is not instantiated by an abstraction term. I think that this is an inadequate condition for classifying the axioms and these and other related questions are the subject of my paper "on existence in set theory", (to appear in notre dame journal of formal logic).