theorem abeqi {x: nat} (p q: wff x): $ p <-> q $ > $ {x | p} == {x | q} $;
p <-> q
T. -> (p <-> q)
T. -> {x | p} == {x | q}
{x | p} == {x | q}