theorem eleq2d (A B: set) (G: wff) (a: nat): $ G -> A == B $ > $ G -> (a e. A <-> a e. B) $;
A == B -> (a e. A <-> a e. B)
G -> A == B
G -> (a e. A <-> a e. B)