Is it true that E [ X | E [ X | Y] ] = Ex [ X | Y] ? Does this law have a name? Let $X$ and $Y$ be two random variables (say real numbers, or vectors in some vector space). It seems to me that the following is true:
E [ X | E [ X | Y ] ] = E [ X | Y]
Note that E [ X | Y ] is a random variable in it's own right. Also note that equality here is point-wise, for every point in the sample space of the joint distribution on on $(X,Y)$. My question, assuming I'm not missing something and the above is true, is whether this law has a name, or is written down / proved somewhere.
 A: Let $Z=E[X\ | \ Y]$. Your equation states: $E[X \ | \ Z]=Z$. This follows from the following fact.
Tower Property of Conditional Expectation:
$$E[E[X\ | \ \mathcal{F}]\ | \ \mathcal{G}]=E[X\ | \ \mathcal{G}],\text{ whenever }\mathcal{G}\subset \mathcal{F}.$$
Proof of your equation:
We apply the tower property with $\mathcal{G}=\sigma(Z)$ and $\mathcal{F}=\sigma(Y)$. Note that $\sigma(Z)\subset \sigma(Y)$ follows from the construction of $Z$ as a conditional expectation w.r.t. $Y$.
Plugging in to the tower property,
$$
\begin{align*}
E[E[X\ | \ \sigma(Y)]\ | \ \sigma(Z)]&=E[X\ | \ \sigma(Z)]\\
\implies E[Z\ | \ Z]&=E[X\ | \ Z]\\
\implies Z&=E[X\ | \ Z].
\end{align*}$$
A: Essentially the law of iterated expectation, perhaps more commonly written like $$\operatorname{E_X} [X] = \operatorname{E}_Y [ \operatorname{E}_{X \mid Y} [ X \mid Y]].$$
For a discrete case, the essence of the proof is 
$$\operatorname{E}_Y [ \operatorname{E}_{X \mid Y} [ X \mid Y]] = \sum_y \sum_x x \cdot \operatorname{P}(X=x \mid Y=y) \cdot \operatorname{P}(Y=y) =\sum_x x \cdot \operatorname{P}(X=x) =\operatorname{E_X} [X].$$
