Weak elimination of imaginaries in the theory of the random graph Let ${\cal U}$ be a countable random graph. Prove that for every formula $\varphi(x)\in L({\cal U})$, where $x$ has arbitrary finite arity, there are a positive integer $n$ and finite $C\subseteq{\cal U}^n$, such that any automorphism of ${\cal U}$ fixes $\varphi({\cal U})$ setwise iff it fixes $C$ setwise.
Motivation The claim above says that the theory of the random graph has weak elimination of imaginaries. This is a well-known fact and the proof should be folklore. But I could only come up with very messy arguments.
 A: Here is an argument using automorphisms. I'm not sure if this is quite as clean an argument as you are looking for, but hopefully it's at least a step in the right direction. Let $D\subseteq\mathcal{U}^k$ be any $\mathcal{U}$-definable set, and choose a subset $A\subset\mathcal{U}$ of minimal possible size over which $D$ is definable. Now, if $B$ is any other set over which $D$ is definable, then by Lemma 2 below $D$ is definable over $A\cap B$, so by minimality of $|A|$ we have $A\subseteq B$. In particular, any automorphism of $\mathcal{U}$ that fixes $D$ setwise must also fix $A$ setwise, so the set $A$ gives the desired parameter for $D$.

Lemma 1: Let $A,B\subset\mathcal{U}$ be finite sets and $\overline{c},\overline{d}\in\mathcal{U}^k$ a pair of $k$-tuples. If $\overline{c}\cap A=\overline{d}\cap B=\varnothing$ and $\overline{c}\equiv_{A\cap B}\overline{d}$, then there exists a $k$-tuple $\overline{e}$ with $\overline{e}\equiv_A\overline{c}$ and $\overline{e}\equiv_B\overline{d}$.
Proof: Proceeding inductively, and replacing $A$ with $A\cup\{c_1,\dots,c_{i-1}\}$ and $B$ with $B\cup\{d_1,\dots,d_{i-1}\}$ at the $i$-th step, we may assume that $k=1$ and thus replace the tuples $\overline{c}$ and $\overline{d}$ with the elements $c=c_1$ and $d=d_1$. Now, write $A=A_0\sqcup A_1$ and $B=B_0\sqcup B_1$, where $A_0$ (resp. $B_0$) is the set of all $a\in A$ (resp. $b\in B$) such that $c R a$ (resp. $d R b$). By quantifier elimination, $\operatorname{tp}(c/A)$ is isolated by $$\{v R a:a\in A_0\}\cup\{\neg(v Ra):a\in A_1\}\cup\{v\neq a:a\in A\},$$ and similarly for $\operatorname{tp}(d/B)$. Hence we need only find an element outside $A\cup B$ that is $R$-related to every element in $A_0\cup B_0$ and not $R$-related to any element in $A_1\cup B_1$, and this is possible by the defining property of the random graph. $\blacksquare$

Lemma 2: Suppose $D$ is $A$-definable and $B$-definable for finite sets $A,B\subset\mathcal{U}$. Then $D$ is $A\cap B$-definable.
Proof: Let $f$ be any automorphism fixing $A\cap B$ pointwise; we want to show that $f$ fixes $D$ setwise. To see this, enumerate $A\setminus B$ as a tuple $\bar{c}$. Since $f$ fixes $A\cap B$, we have $f(\bar{c})\cap (A\cap B)=\varnothing$, so we may find a conjugate $\bar{c}'\equiv_B f(\bar{c})$ with $\bar{c}'\cap A=\varnothing$. Let $g$ be any automorphism fixing $B$ pointwise and taking $f(\bar{c})$ to $\bar{c}'$; then $g$ fixes $D$ setwise.
Since $\bar{c}'\cap A=\varnothing$ and $\bar{c}\cap B=\varnothing$, and $\bar{c}$ and $\bar{c}'$ are conjugate by the $(A\cap B)$-automorphism $g\circ f$, by Lemma 1 we may find a tuple $\bar{c}''$ with $\bar{c}'\equiv_A\bar{c}''$ and $\bar{c}''\equiv_B \bar{c}$. Let $h$ be the composition of any two automorphisms witnessing these; since $h$ is the composition of an automorphism fixing $A$ pointwise and one fixing $B$ pointwise, we have that $h$ fixes $A\cap B$ pointwise and fixes $D$ setwise. On the other hand, $h$ takes $\bar{c}'=g(f(\bar{c}))$ to $\bar{c}$, whence $h\circ g\circ f$ fixes $A\setminus B$ pointwise. So $h\circ g\circ f$ fixes $A$ pointwise, and hence fixes $D$ setwise. Since $h\circ g$ fixes $D$ setwise as well, this means that $f$ does too, as desired. $\blacksquare$
