theorem eqrd (A B: set) (G: wff) {x: nat}: $ G -> (x e. A <-> x e. B) $ > $ G -> A == B $;
G -> (x e. A <-> x e. B)
G -> A. x (x e. A <-> x e. B)
G -> A == B