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