Trying to correct code with the suggestions. I didn't see how I could use MemberQ; so I used Element. How would you tweak the code below to get a proof that {1,2,3} = {3,2,1}.

axiom2 = ForAll[{x, y}, 
   Implies[ForAll[z, Equivalent[Element[z, x], Element[z, y]]], 
    x === y]];
seta = {1, 2, 3};
setb = {3, 2, 1};
FindEquationalProof[seta === setb, axiom2]

There are some problems

• You used \[Epsilon]. It is just a symbol, you are looking for MemberQ
• you used == (i.e., Equal) when you put seta == setb automatically the operation will be evaluated as False. So just make some symbolic function that will denotes the two sets are identical or equal (eg., eq[x,y])
• Last one, Implies[False, True] returns True meaning that if there is some z that belongs to set y but not to set x the relation is still True... so the "axiom" is practically ForAll[{x,y}, eq[x,y]] regardless of z, so ANY two sets are defined equal by the presented logic of this expression

You need another way to define the relation...

best