theorem eqab1i (A: set) {x: nat} (p: wff x): $ p <-> x e. A $ > $ {x | p} == A $;
p <-> x e. A
T. -> (p <-> x e. A)
T. -> {x | p} == A
{x | p} == A