Hierarchy of undecidable languages

Let us define two languages of Turing machines.
$$
EQ_{TM} = \{ : L(M_1) = L(M_2)\}
$$
$$
ALL_{TM} = \{ : L(M) = \Sigma^*\}
$$
It is easy to show that neither of the languages are in $RE \cup coRE$, and also it is easy to construct a reduction $ALL_{TM} \leq EQ_{TM}$.

I suspect that there is no reduction in the other direction, but I don't know how to prove it. Is there some sort of hierarchy of undecidable/non-recognizable languages that proves it?

Let's fix the following definition for $L(M)$: it's the set of strings $x$ such that $M$ halts on input $x$.

Given machines $M_1,M_2$, consider a machine $M$ which accepts two inputs $x$ and $t$ and runs the following algorithm:

• Run $M_1$ on input $x$ for $t$ steps.

• If $M_1$ halted: run $M_2$ on $x$.

• Otherwise:

• Run $M_2$ on input $x$ for $t$ steps.

• If $M_2$ halted: run $M_1$ on $x$.

• Otherwise: halt.

The machine $M$ rejects an input $x,t$ iff one of the machines $M_1,M_2$ accepts $x$ within $t$ steps and the other one rejects $x$. So $M$ accepts all inputs iff $L(M_1) = L(M_2)$.

StackExchange Computer Science Q#12939, answer score: 5