Consider a pure exchange economy with $N\geq2$ consumers, each of whom has locally non-satiated preferences. We know from the First Welfare Theorem that any Walrasian equilibrium is Pareto-efficient. We index consumers by superscripts.
Say that consumer $i$ envies consumer $j$'s allocation if $i$ strictly prefers $j$'s allocation to their own:
$$ x^j \succ^i x^i $$
If these preferences have a utility representation, then this is equivalent to
$$ u^i (x^j) > u^i(x^i) $$
It is an easy consequence of the First Welfare Theorem that in any Walrasian equilibrium, no two agents, regardless of income, envy each other's allocations. If they did, this would violate Pareto-efficiency.
Notice, however, that this is not the same as the allocation being envy-free.