Definable and $A$-invariant set is $A$-definable. I know that this is a well known fact in model theory but I can not find a complete proof.
Let $A\subseteq \mathfrak{C}$ a small subset and $U\subseteq \mathfrak{C}$ a definable set. If $U$ is $A$-invariant (invariant under $Aut(\mathfrak{C}/A)$) then it is $A$-definable.
I tried assuming that we needed parameters outside of $A$ to get a contradiction with $A$-invariance but I am not able to finish the proof.
Also, is this still true if we replace definable set with type-definable set?
 A: There is a proof of this fact in A Course in Model Theory by Tent and Ziegler, Lemma 6.1.10. That proof is topological in nature, so I will translate it to logical terms here. Along the way we will also take a look at type-definable sets.
Claim 1. If $U$ is a type-definable $A$-invariant set then $U$ is type-definable over $A$.
Proof. Let $\pi(x)$ be a partial type over some $B$ defining $U$. We claim that the following partial type defines $U$:
$$
\Sigma(x) = \{ \psi(x, a) : a \in A \text{ and } \models \psi(c, a) \text{ for all } c \in U \}.
$$
Clearly, if $c \in U$ then $\models \Sigma(c)$. For the other direction, we assume that $c$ is such that $\models \Sigma(c)$ and we claim that $\operatorname{tp}(c/A) \cup \pi(x)$ is consistent. If not, then there is $\chi(x) \in \operatorname{tp}(c/A)$ such that $\pi(x)$ is inconsistent with $\chi(x)$. Then by construction $\neg \chi(x) \in \Sigma(x)$, but this contradicts $\Sigma(x) \subseteq \operatorname{tp}(c/A)$. So let $c'$ realise $\operatorname{tp}(c/A) \cup \pi(x)$. Then $c' \in U$ while $\operatorname{tp}(c/A) = \operatorname{tp}(c'/A)$, so by $A$-invariance $c \in U$, as required.
So the above claim already answers your question for type-definable sets. We can use the claim to show that if $U$ is actually definable, that then $\Sigma(x)$ can be assumed to be a formula.
Claim 2. If $U$ is a definable $A$-invariant set then $U$ is definable over $A$.
Proof. Let $\phi(x, b)$ define $U$. We apply claim 1 with $\pi(x) = \{\phi(x, b)\}$ to find a partial type $\Sigma(x)$ over $A$ that defines $U$. So clearly $\phi(x, b)$ implies $\Sigma(x)$. We have that $\Sigma(x)$ is inconsistent with $\neg \phi(x, b)$. So there is $\psi(x, a) \in \Sigma(x)$ that is inconsistent with $\neg \phi(x, b)$ (we may assume $\Sigma(x)$ to be closed under conjunctions). So $\psi(x, a)$ implies $\phi(x, b)$ and we see that $\psi(x, a)$ defines $U$.
