What am I doing wrong here?
axiom0 = ForAll[{x, y},
ForAll[z, Implies[Equivalent[z\[Epsilon]x, z\[Epsilon]y], x == y]]]
seta = {1, 2, 3};
setb = {3, 2 , 1};
FindEquationalProof[seta == setb, axiom0]
I am attempting to write an extensionality axiom followed by a proof that {1,2,3} = {3,2,1}
. Here, [Epsilon] denotes set membership.
Thanks!
It's not working. Any advice?