MemberQ
will evaluate to False
before ForAll
ever sees it. THe following will show this.
Exists[z, MemberQ[Y, z], ForAll[u, MemberQ[X, u], z == u]] // Trace
What is needed is an "algebraicization" of the membership relation. This can be done as below, by setting the product of differences x-elementj
to zero.
xX = {3, 3, 3};
yY = {1, 2, 3};
myElement[x_, set_] := Apply[Times, x - set] == 0
Resolve
is needed for quantifier elimination.
Resolve[
ForAll[x, myElement[x, xX], Exists[y, myElement[y, yY], x == y]]]
(* Out[304]= True *)
Resolve[
Exists[z, myElement[z, yY], ForAll[u, myElement[u, xX], z == u]]]
(* Out[303]= True *)
If the sets in question are consecutive integers the element check can be done instead via inequalities with a subsequent domain restriction for Resolve
.
myElement2[x_, set_] := Min[set] <= x <= Max[set]
Resolve[Exists[z, myElement2[z, yY],
ForAll[u, myElement2[u, xX], z == u]], Integers]
(* Out[310]= True *)
Alternatively the domain restriction can be placed directly in the element test:
myElement3[x_, set_] :=
Min[set] <= x <= Max[set] && Element[x, Integers]
Resolve[Exists[z, myElement3[z, yY],
ForAll[u, myElement3[u, xX], z == u]]]
(* Out[314]= True *)