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