Why Can't Mathematica Resolve this Simple Quantified Expression?

Question

I've been using Mathematica as a hobbyist, off and on, for some time. So while I'm by no means an expert I've used it long enough to know that what might seem obvious to me is not necessarily obvious to the program. I'm hoping for an answer that will provide me a better understanding of how to 'approach' the software in this case:

Why can't Mathematica resolve this rather obvious quantified expression?

Resolve[ForAll[{x, y}, x^y == y^x], Reals]

which just returns (after thinking for a while) $ \forall _{\{x,y\}} x^y = y^x $. But I provide a 'hint' it will return immediately:

Resolve[ForAll[{x, y}, y == 2 ∧ x^y == y^x], Reals]
False

I think that if I understood Resolve's internal algorithm better, I could probably phrase the problem in a better way. Why isn't my 'naive' phrasing of the problem useable by Mathematica?

Answer 1

There is a workaround.

ClearAll[x, y]; ForAll[{x, y}, x > 0 && y > 0, x*Log[y] == y*Log[x]];Resolve[%, Reals]

False

Answer 2

ContourPlot might help a little bit:

ContourPlot[x^y == y^x, {x, 0, 2}, {y, 0, 2}, MaxRecursion -> 5,FrameLabel -> {x, y}]    

The only real solution(x>0,y>0) seems to be x==y

Answer 3

Thank you both '64494 and Ulrich for your answers; which both were much better approaches to finding solutions to that particular problem.

Ultimately I was trying to understand what I was doing 'wrong' that made the Resolve/ForAll approach fail so badly. While I have great respect for Mathematica as a product, and there are obviously certain things that it does very well, that doesn't appear to encompass much of general theorem proving. After struggling with it some more, I've come to the conclusion that the 'Details and Options' section offers some clue as to what will (and by implication, what will not) work well:

Resolve[expr] can in principle always eliminate quantifiers if expr contains only polynomial equations and inequalities over the reals or complexes.

Resolve[expr] can in principle always eliminate quantifiers for any Boolean expression expr.