ReplaceAll works and does not work for the same expression

I will give two cases, where the rule replacement works in the first one and does not work in the second one, but they are essentially the same!

Consider the following definition, whose details are not important:

vall = -Sqrt[Δ^2 + μ^2 + 2*μ*Sqrt[px^2 + py^2] + px^2 + py^2]


Now, we check the following:

vall /. {ϕ -> 0, py -> pyy, px -> 0, μ -> 0}


As expected, I can obtain the desired replacement:

Now, consider the following expression, which contains the above expression as a subexpression:

Exists[
{py, pyy},
123 == (vall /. {ϕ -> 0, py -> pyy, px -> 0, μ -> 0}) == 0  ]


The result is surprising:

As can be seen in the picture, no replacement py -> pyy is made!

Why does this happen?

• You should condense your problem to a much smaller, minimal working example that reproduces the behavior you see. – MarcoB Mar 29 at 3:19
• @MarcoB I simplified the code. – eigenvalue Mar 29 at 7:12
• After printing vars like Exists[{py, pyy}, Print[{py, pyy}]; 123 == (vall /. {[Phi] -> 0, py -> pyy, px -> 0, [Mu] -> 0}) == 0] your will note that Exists renamed vars. So, substitution simply do not mach pattern. – Acus Mar 29 at 8:01

I suspect that this has to do with the HoldAll attribute of Exists (see Attributes[Exists]). However, if you force evaluation of its second argument, i.e. the expression you are trying to modify, you obtain the desired result:
Exists[